Theorem vtoclbg 3172

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115

This theorem is referenced by:  alexeqg  3232  pm13.183  3244  sbc8g  3339  sbc2or  3340  sbcco  3354  sbc5  3356  sbcie2g  3365  eqsbc3  3371  sbcng  3372  sbcimg  3373  sbcan  3374  sbcangOLD  3375  sbcor  3376  sbcorgOLD  3377  sbcbig  3378  sbcal  3383  sbcalgOLD  3384  sbcex2  3385  sbcexgOLD  3386  sbc3angOLD  3395  sbcel1v  3396  sbcel1gvOLD  3397  sbcrexgOLD  3417  sbcreu  3418  sbcreugOLD  3419  csbiebg  3458  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  elpwg  4018  snssg  4160  preq12bg  4205  elintg  4290  elintrabg  4295  sbcbr123  4498  sbcbrgOLD  4499  opelresg  5281  funfvima3  6137  elixpsn  7508  ixpsnf1o  7509  domeng  7530  1sdom  7722  rankcf  9155  pt1hmeo  20070  eldm3  28796  elima4  28814  brsset  29144  brbigcup  29153  elfix2  29159  elfunsg  29171  elsingles  29173  funpartlem  29197  ellines  29407  elhf2g  29438  cover2g  29836  inisegn0  30621