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

Metamath Proof Explorer

Theorem vtocl2d

Description: Implicit substitution of two classes for two setvar variables. (Contributed by Thierry Arnoux, 25-Aug-2020) (Revised by BTernaryTau, 19-Oct-2023)

Ref Expression
Hypotheses vtocl2d.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
vtocl2d.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
vtocl2d.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
vtocl2d.3 ⊢ ( 𝜑 → 𝜓 )
Assertion vtocl2d ( 𝜑 → 𝜒 )

Proof

Step Hyp Ref Expression
1 vtocl2d.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 vtocl2d.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 vtocl2d.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
4 vtocl2d.3 ⊢ ( 𝜑 → 𝜓 )
5 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → 𝜓 )
6 3 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
7 6 pm5.74da ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝑦 = 𝐵 → 𝜓 ) ↔ ( 𝑦 = 𝐵 → 𝜒 ) ) )
8 4 a1d ⊢ ( 𝜑 → ( 𝑦 = 𝐵 → 𝜓 ) )
9 1 7 8 vtocld ⊢ ( 𝜑 → ( 𝑦 = 𝐵 → 𝜒 ) )
10 9 imp ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → 𝜒 )
11 5 10 2thd ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
12 2 11 4 vtocld ⊢ ( 𝜑 → 𝜒 )