Metamath Proof Explorer

Theorem dfon2lem1

Description: Lemma for dfon2 . (Contributed by Scott Fenton, 28-Feb-2011) (Proof shortened by SN, 5-Oct-2026)

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 simp2 ⊢ φ ∧ Tr ⁡ x ∧ ψ → Tr ⁡ x
3 2 ss2abi ⊢ x | φ ∧ Tr ⁡ x ∧ ψ ⊆ x | Tr ⁡ x
4 3 sseli ⊢ y ∈ x | φ ∧ Tr ⁡ x ∧ ψ → y ∈ x | Tr ⁡ x
5 vex ⊢ y ∈ V
6 treq ⊢ x = y → Tr ⁡ x ↔ Tr ⁡ y
7 5 6 elab ⊢ y ∈ x | Tr ⁡ x ↔ Tr ⁡ y
8 4 7 sylib ⊢ y ∈ x | φ ∧ Tr ⁡ x ∧ ψ → Tr ⁡ y
9 1 8 mprg ⊢ Tr ⁡ ⋃ x | φ ∧ Tr ⁡ x ∧ ψ