---

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


1. [P] : ℙ
2. [Q] : ℙ
3. ⋂:P. Q@i
4. [%2] : P@i
⊢ Q
BY
{ (RenameVar `x' (-2) THEN UseWitness ⌜x⌝⋅) }

1
1. P : ℙ
2. Q : ℙ
3. x : ⋂:P. Q@i
4. P@i
⊢ x ∈ Q

---

Latex:

---

Latex:

1.  [P]  :  \mBbbP{}
2.  [Q]  :  \mBbbP{}
3.  \mcap{}:P.  Q@i
4.  [\%2]  :  P@i
\mvdash{}  Q


By

---

Latex:
(RenameVar  `x'  (-2)  THEN  UseWitness  \mkleeneopen{}x\mkleeneclose{}\mcdot{})

---

Home Index