Theorem vtoclbg 3093

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 319	. 2 |- ( x = A -> ( ( ph <-> ps ) <-> ( ch <-> th ) ) )
4		vtoclbg.3	. 2 |- ( ph <-> ps )
5	3, 4	vtoclg 3092	1 |- ( A e. V -> ( ch <-> th ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1399   e. wcel 1826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-12 1862  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-v 3036

This theorem is referenced by:  alexeqg  3153  pm13.183  3165  sbc8g  3260  sbc2or  3261  sbcco  3275  sbc5  3277  sbcie2g  3286  eqsbc3  3292  sbcng  3293  sbcimg  3294  sbcan  3295  sbcor  3296  sbcbig  3297  sbcal  3302  sbcex2  3303  sbcel1v  3311  sbcreu  3329  csbiebg  3371  sbcel12  3750  sbceqg  3751  elpwg  3935  snssg  4077  preq12bg  4123  elintg  4207  elintrabg  4212  sbcbr123  4418  opelresg  5193  funfvima3  6050  elixpsn  7427  ixpsnf1o  7428  domeng  7449  1sdom  7639  rankcf  9066  pt1hmeo  20392  eldm3  29357  elima4  29374  brsset  29692  brbigcup  29701  elfix2  29707  elfunsg  29719  elsingles  29721  funpartlem  29745  ellines  29955  elhf2g  29986  cover2g  30371  sbcrexgOLD  30884  inisegn0  31155  sbcangOLD  33636  sbcorgOLD  33637  sbcalgOLD  33649  sbcexgOLD  33650  sbcel12gOLD  33651  sbcel1gvOLD  34005