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

Metamath Proof Explorer

Theorem vtocl3gf

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013) (Revised by Mario Carneiro, 10-Oct-2016)

Ref Expression
Hypotheses vtocl3gf.a 
|- F/_ x A
vtocl3gf.b 
|- F/_ y A
vtocl3gf.c 
|- F/_ z A
vtocl3gf.d 
|- F/_ y B
vtocl3gf.e 
|- F/_ z B
vtocl3gf.f 
|- F/_ z C
vtocl3gf.1 
|- F/ x ps
vtocl3gf.2 
|- F/ y ch
vtocl3gf.3 
|- F/ z th
vtocl3gf.4 
|- ( x = A -> ( ph <-> ps ) )
vtocl3gf.5 
|- ( y = B -> ( ps <-> ch ) )
vtocl3gf.6 
|- ( z = C -> ( ch <-> th ) )
vtocl3gf.7 
|- ph
Assertion vtocl3gf 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> th )

Proof

Step Hyp Ref Expression
1 vtocl3gf.a 
 |-  F/_ x A
2 vtocl3gf.b 
 |-  F/_ y A
3 vtocl3gf.c 
 |-  F/_ z A
4 vtocl3gf.d 
 |-  F/_ y B
5 vtocl3gf.e 
 |-  F/_ z B
6 vtocl3gf.f 
 |-  F/_ z C
7 vtocl3gf.1 
 |-  F/ x ps
8 vtocl3gf.2 
 |-  F/ y ch
9 vtocl3gf.3 
 |-  F/ z th
10 vtocl3gf.4 
 |-  ( x = A -> ( ph <-> ps ) )
11 vtocl3gf.5 
 |-  ( y = B -> ( ps <-> ch ) )
12 vtocl3gf.6 
 |-  ( z = C -> ( ch <-> th ) )
13 vtocl3gf.7 
 |-  ph
14 elex 
 |-  ( A e. V -> A e. _V )
15 2 nfel1 
 |-  F/ y A e. _V
16 15 8 nfim 
 |-  F/ y ( A e. _V -> ch )
17 3 nfel1 
 |-  F/ z A e. _V
18 17 9 nfim 
 |-  F/ z ( A e. _V -> th )
19 11 imbi2d 
 |-  ( y = B -> ( ( A e. _V -> ps ) <-> ( A e. _V -> ch ) ) )
20 12 imbi2d 
 |-  ( z = C -> ( ( A e. _V -> ch ) <-> ( A e. _V -> th ) ) )
21 1 7 10 13 vtoclgf 
 |-  ( A e. _V -> ps )
22 4 5 6 16 18 19 20 21 vtocl2gf 
 |-  ( ( B e. W /\ C e. X ) -> ( A e. _V -> th ) )
23 14 22 mpan9 
 |-  ( ( A e. V /\ ( B e. W /\ C e. X ) ) -> th )
24 23 3impb 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> th )