Theorem vtoclbg 3108

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

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   e. wcel 1887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-v 3047

This theorem is referenced by:  alexeqg  3168  pm13.183  3179  sbc8g  3275  sbc2or  3276  sbcco  3290  sbc5  3292  sbcie2g  3301  eqsbc3  3307  sbcng  3308  sbcimg  3309  sbcan  3310  sbcor  3311  sbcbig  3312  sbcal  3317  sbcex2  3318  sbcel1v  3326  sbcreu  3344  csbiebg  3386  sbcel12  3772  sbceqg  3773  elpwg  3959  snssg  4105  preq12bg  4154  elintg  4242  elintrabg  4247  sbcbr123  4454  opelresg  5112  inisegn0  5200  funfvima3  6142  elixpsn  7561  ixpsnf1o  7562  domeng  7583  1sdom  7775  rankcf  9202  pt1hmeo  20821  eldm3  30402  br1steqg  30416  br2ndeqg  30417  elima4  30421  brsset  30656  brbigcup  30665  elfix2  30671  elfunsg  30683  elsingles  30685  funpartlem  30709  ellines  30919  elhf2g  30943  cover2g  32041  sbcrexgOLD  35628  sbcangOLD  36890  sbcorgOLD  36891  sbcalgOLD  36903  sbcexgOLD  36904  sbcel12gOLD  36905  sbcel1gvOLD  37255