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 _ x A
vtocl2gaf.b _ y A
vtocl2gaf.c _ y B
vtocl2gaf.1 x ψ
vtocl2gaf.2 y χ
vtocl2gaf.3 x = A φ ψ
vtocl2gaf.4 y = B ψ χ
vtocl2gaf.5 x C y D φ
Assertion vtocl2gaf A C B D χ

Proof

Step Hyp Ref Expression
1 vtocl2gaf.a _ x A
2 vtocl2gaf.b _ y A
3 vtocl2gaf.c _ y B
4 vtocl2gaf.1 x ψ
5 vtocl2gaf.2 y χ
6 vtocl2gaf.3 x = A φ ψ
7 vtocl2gaf.4 y = B ψ χ
8 vtocl2gaf.5 x C y D φ
9 2 nfel1 y A C
10 9 5 nfim y A C χ
11 7 imbi2d y = B A C ψ A C χ
12 nfv x y D
13 12 4 nfim x y D ψ
14 6 imbi2d x = A y D φ y D ψ
15 8 ex x C y D φ
16 1 13 14 15 vtoclgaf A C y D ψ
17 16 com12 y D A C ψ
18 3 10 11 17 vtoclgaf B D A C χ
19 18 impcom A C B D χ