Metamath Proof Explorer


Theorem vtocl2gaf

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013) (Proof shortened by Wolf Lammen, 31-May-2025)

Ref Expression
Hypotheses vtocl2gaf.a 𝑥 𝐴
vtocl2gaf.b 𝑦 𝐴
vtocl2gaf.c 𝑦 𝐵
vtocl2gaf.1 𝑥 𝜓
vtocl2gaf.2 𝑦 𝜒
vtocl2gaf.3 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
vtocl2gaf.4 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) )
vtocl2gaf.5 ( ( 𝑥𝐶𝑦𝐷 ) → 𝜑 )
Assertion vtocl2gaf ( ( 𝐴𝐶𝐵𝐷 ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 vtocl2gaf.a 𝑥 𝐴
2 vtocl2gaf.b 𝑦 𝐴
3 vtocl2gaf.c 𝑦 𝐵
4 vtocl2gaf.1 𝑥 𝜓
5 vtocl2gaf.2 𝑦 𝜒
6 vtocl2gaf.3 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
7 vtocl2gaf.4 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) )
8 vtocl2gaf.5 ( ( 𝑥𝐶𝑦𝐷 ) → 𝜑 )
9 2 nfel1 𝑦 𝐴𝐶
10 9 5 nfim 𝑦 ( 𝐴𝐶𝜒 )
11 7 imbi2d ( 𝑦 = 𝐵 → ( ( 𝐴𝐶𝜓 ) ↔ ( 𝐴𝐶𝜒 ) ) )
12 nfv 𝑥 𝑦𝐷
13 12 4 nfim 𝑥 ( 𝑦𝐷𝜓 )
14 6 imbi2d ( 𝑥 = 𝐴 → ( ( 𝑦𝐷𝜑 ) ↔ ( 𝑦𝐷𝜓 ) ) )
15 8 ex ( 𝑥𝐶 → ( 𝑦𝐷𝜑 ) )
16 1 13 14 15 vtoclgaf ( 𝐴𝐶 → ( 𝑦𝐷𝜓 ) )
17 16 com12 ( 𝑦𝐷 → ( 𝐴𝐶𝜓 ) )
18 3 10 11 17 vtoclgaf ( 𝐵𝐷 → ( 𝐴𝐶𝜒 ) )
19 18 impcom ( ( 𝐴𝐶𝐵𝐷 ) → 𝜒 )