Theorem vtoclbg 3154

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 3153	1 |- ( A e. V -> ( ch <-> th ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1383   e. wcel 1804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097

This theorem is referenced by:  alexeqg  3214  pm13.183  3226  sbc8g  3321  sbc2or  3322  sbcco  3336  sbc5  3338  sbcie2g  3347  eqsbc3  3353  sbcng  3354  sbcimg  3355  sbcan  3356  sbcangOLD  3357  sbcor  3358  sbcorgOLD  3359  sbcbig  3360  sbcal  3365  sbcalgOLD  3366  sbcex2  3367  sbcexgOLD  3368  sbc3angOLD  3377  sbcel1v  3378  sbcel1gvOLD  3379  sbcrexgOLD  3399  sbcreu  3400  sbcreugOLD  3401  csbiebg  3443  sbcel12  3809  sbcel12gOLD  3810  sbceqg  3811  elpwg  4005  snssg  4148  preq12bg  4194  elintg  4279  elintrabg  4284  sbcbr123  4488  sbcbrgOLD  4489  opelresg  5271  funfvima3  6134  elixpsn  7510  ixpsnf1o  7511  domeng  7532  1sdom  7724  rankcf  9158  pt1hmeo  20284  eldm3  29166  elima4  29184  brsset  29514  brbigcup  29523  elfix2  29529  elfunsg  29541  elsingles  29543  funpartlem  29567  ellines  29777  elhf2g  29808  cover2g  30180  inisegn0  30964