---

Step * 1 1 1 of Lemma uimplies-iff-squash-implies


1. P : ℙ
2. Q : ℙ
3. x : ⋂:P. Q@i
4. P@i
⊢ x ∈ Q
BY
{ (RenameVar `a' (-1) THEN With ⌜a⌝ (DVar `x')⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  P  :  \mBbbP{}
2.  Q  :  \mBbbP{}
3.  x  :  \mcap{}:P.  Q@i
4.  P@i
\mvdash{}  x  \mmember{}  Q


By

---

Latex:
(RenameVar  `a'  (-1)  THEN  With  \mkleeneopen{}a\mkleeneclose{}  (DVar  `x')\mcdot{}  THEN  Auto)

---

Home Index