Metamath Proof Explorer

Theorem vtocl3g

Description: Implicit substitution of a class for a setvar variable. Version of vtocl3gf with disjoint variable conditions instead of nonfreeness hypotheses, requiring fewer axioms. (Contributed by GG, 3-Oct-2024)

Ref Expression
Hypotheses vtocl3g.1 ⊢ x = A → φ ↔ ψ
vtocl3g.2 ⊢ y = B → ψ ↔ χ
vtocl3g.3 ⊢ z = C → χ ↔ θ
vtocl3g.4 ⊢ φ
Assertion vtocl3g ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → θ

Proof

Step Hyp Ref Expression
1 vtocl3g.1 ⊢ x = A → φ ↔ ψ
2 vtocl3g.2 ⊢ y = B → ψ ↔ χ
3 vtocl3g.3 ⊢ z = C → χ ↔ θ
4 vtocl3g.4 ⊢ φ
5 elex ⊢ A ∈ V → A ∈ V
6 2 imbi2d ⊢ y = B → A ∈ V → ψ ↔ A ∈ V → χ
7 3 imbi2d ⊢ z = C → A ∈ V → χ ↔ A ∈ V → θ
8 1 4 vtoclg ⊢ A ∈ V → ψ
9 6 7 8 vtocl2g ⊢ B ∈ W ∧ C ∈ X → A ∈ V → θ
10 5 9 mpan9 ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → θ
11 10 3impb ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → θ