Metamath Proof Explorer

Theorem dfon2lem1

Description: Lemma for dfon2 . (Contributed by Scott Fenton, 28-Feb-2011)

Ref Expression
Assertion dfon2lem1 ⊢ Tr ⁡ ⋃ x | φ ∧ Tr ⁡ x ∧ ψ

Proof

Step Hyp Ref Expression
1 truni ⊢ ∀ y ∈ x | φ ∧ Tr ⁡ x ∧ ψ Tr ⁡ y → Tr ⁡ ⋃ x | φ ∧ Tr ⁡ x ∧ ψ
2 nfsbc1v ⊢ Ⅎ x [˙y / x]˙ φ
3 nfv ⊢ Ⅎ x Tr ⁡ y
4 nfsbc1v ⊢ Ⅎ x [˙y / x]˙ ψ
5 2 3 4 nf3an ⊢ Ⅎ x [˙y / x]˙ φ ∧ Tr ⁡ y ∧ [˙y / x]˙ ψ
6 vex ⊢ y ∈ V
7 sbceq1a ⊢ x = y → φ ↔ [˙y / x]˙ φ
8 treq ⊢ x = y → Tr ⁡ x ↔ Tr ⁡ y
9 sbceq1a ⊢ x = y → ψ ↔ [˙y / x]˙ ψ
10 7 8 9 3anbi123d ⊢ x = y → φ ∧ Tr ⁡ x ∧ ψ ↔ [˙y / x]˙ φ ∧ Tr ⁡ y ∧ [˙y / x]˙ ψ
11 5 6 10 elabf ⊢ y ∈ x | φ ∧ Tr ⁡ x ∧ ψ ↔ [˙y / x]˙ φ ∧ Tr ⁡ y ∧ [˙y / x]˙ ψ
12 11 simp2bi ⊢ y ∈ x | φ ∧ Tr ⁡ x ∧ ψ → Tr ⁡ y
13 1 12 mprg ⊢ Tr ⁡ ⋃ x | φ ∧ Tr ⁡ x ∧ ψ