---

Step * of Lemma free-from-atom-pair-components

∀[a:Atom1]. ∀[X:Type]. ∀[Y:X ⟶ 𝕌']. ∀[x:X]. ∀[y:Y[x]].  {a#x:X ∧ a#y:Y[x]} supposing a#<x, y>:x:X × Y[x]
BY
{ (UniformUnivCD Auto THEN D 0) }

1
1. a : Atom1
2. X : Type
3. Y : X ⟶ 𝕌'
4. x : X
5. y : Y[x]
6. a#<x, y>:x:X × Y[x]
⊢ a#x:X

2
1. a : Atom1
2. X : Type
3. Y : X ⟶ 𝕌'
4. x : X
5. y : Y[x]
6. a#<x, y>:x:X × Y[x]
⊢ a#y:Y[x]

---

Latex:

---

Latex:
\mforall{}[a:Atom1].  \mforall{}[X:Type].  \mforall{}[Y:X  {}\mrightarrow{}  \mBbbU{}'].  \mforall{}[x:X].  \mforall{}[y:Y[x]].    \{a\#x:X  \mwedge{}  a\#y:Y[x]\}  supposing  a\#<x,  y>:x:X  \mtimes{}\000C  Y[x]


By

---

Latex:
(UniformUnivCD  Auto  THEN  D  0)

---

Home Index