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

Metamath Proof Explorer

Theorem vtocl2

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011)

Ref Expression
Hypotheses vtocl2.1 ⊢ 𝐴 ∈ V
vtocl2.2 ⊢ 𝐵 ∈ V
vtocl2.3 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
vtocl2.4 ⊢ 𝜑
Assertion vtocl2 𝜓

Proof

Step Hyp Ref Expression
1 vtocl2.1 ⊢ 𝐴 ∈ V
2 vtocl2.2 ⊢ 𝐵 ∈ V
3 vtocl2.3 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
4 vtocl2.4 ⊢ 𝜑
5 4 a1i ⊢ ( 𝑦 = 𝐵 → 𝜑 )
6 3 pm5.74da ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 = 𝐵 → 𝜑 ) ↔ ( 𝑦 = 𝐵 → 𝜓 ) ) )
7 1 6 5 vtocl ⊢ ( 𝑦 = 𝐵 → 𝜓 )
8 5 7 2thd ⊢ ( 𝑦 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
9 2 8 4 vtocl ⊢ 𝜓