This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtocl3

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011) Avoid ax-10 and ax-11 . (Revised by GG, 20-Aug-2023) (Proof shortened by Wolf Lammen, 23-Aug-2023)

Ref Expression
Hypotheses vtocl3.1 ⊢ A ∈ V
vtocl3.2 ⊢ B ∈ V
vtocl3.3 ⊢ C ∈ V
vtocl3.4 ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
vtocl3.5 ⊢ φ
Assertion vtocl3 ⊢ ψ

Proof

Step Hyp Ref Expression
1 vtocl3.1 ⊢ A ∈ V
2 vtocl3.2 ⊢ B ∈ V
3 vtocl3.3 ⊢ C ∈ V
4 vtocl3.4 ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
5 vtocl3.5 ⊢ φ
6 5 a1i ⊢ z = C → φ
7 4 3expa ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
8 7 pm5.74da ⊢ x = A ∧ y = B → z = C → φ ↔ z = C → ψ
9 1 2 8 6 vtocl2 ⊢ z = C → ψ
10 6 9 2thd ⊢ z = C → φ ↔ ψ
11 3 10 5 vtocl ⊢ ψ