Theorem vtoclbg 2799

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	|- ( x = A -> ( ph <-> ch ) )
vtoclbg.2	|- ( x = A -> ( ps <-> th ) )
vtoclbg.3	|- ( ph <-> ps )

Assertion

Ref	Expression
vtoclbg	|- ( A e. V -> ( ch <-> th ) )

Distinct variable groups:   x, A   ch, x   th, x

Allowed substitution hints:   ph( x)   ps( x)   V( x)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 |- ( x = A -> ( ph <-> ch ) )
2		vtoclbg.2	. . 3 |- ( x = A -> ( ps <-> th ) )
3	1, 2	bibi12d 235	. 2 |- ( x = A -> ( ( ph <-> ps ) <-> ( ch <-> th ) ) )
4		vtoclbg.3	. 2 |- ( ph <-> ps )
5	3, 4	vtoclg 2798	1 |- ( A e. V -> ( ch <-> th ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   e. wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740

This theorem is referenced by:  pm13.183  2876  sbc8g  2971  sbcco  2985  sbc5  2987  sbcie2g  2997  eqsbc1  3003  sbcng  3004  sbcimg  3005  sbcan  3006  sbcang  3007  sbcor  3008  sbcorg  3009  sbcbig  3010  sbcal  3015  sbcalg  3016  sbcex2  3017  sbcexg  3018  sbcel1v  3026  sbcralg  3042  sbcreug  3044  sbcel12g  3073  sbceqg  3074  csbiebg  3100  elpwg  3584  snssgOLD  3729  preq12bg  3774  elintg  3853  elintrabg  3858  sbcbrg  4058  opelresg  4915  elixpsn  6735  ixpsnf1o  6736  domeng  6752