Theorem vtoclbg 3094

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

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1452   e. wcel 1904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-v 3033

This theorem is referenced by:  alexeqg  3156  pm13.183  3167  sbc8g  3263  sbc2or  3264  sbcco  3278  sbc5  3280  sbcie2g  3289  eqsbc3  3295  sbcng  3296  sbcimg  3297  sbcan  3298  sbcor  3299  sbcbig  3300  sbcal  3305  sbcex2  3306  sbcel1v  3314  sbcreu  3332  csbiebg  3372  sbcel12  3776  sbceqg  3777  elpwg  3950  snssg  4096  preq12bg  4146  elintg  4234  elintrabg  4239  sbcbr123  4447  opelresg  5118  inisegn0  5206  funfvima3  6160  elixpsn  7579  ixpsnf1o  7580  domeng  7601  1sdom  7793  rankcf  9220  pt1hmeo  20898  eldm3  30473  br1steqg  30487  br2ndeqg  30488  elima4  30492  brsset  30727  brbigcup  30736  elfix2  30742  elfunsg  30754  elsingles  30756  funpartlem  30780  ellines  30990  elhf2g  31014  cover2g  32105  sbcrexgOLD  35699  sbcangOLD  36960  sbcorgOLD  36961  sbcalgOLD  36973  sbcexgOLD  36974  sbcel12gOLD  36975  sbcel1gvOLD  37318