Theorem vtoclbg 2702

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1299   e. wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643

This theorem is referenced by:  pm13.183  2776  sbc8g  2869  sbcco  2883  sbc5  2885  sbcie2g  2894  eqsbc3  2900  sbcng  2901  sbcimg  2902  sbcan  2903  sbcang  2904  sbcor  2905  sbcorg  2906  sbcbig  2907  sbcal  2912  sbcalg  2913  sbcex2  2914  sbcexg  2915  sbcel1v  2923  sbcralg  2939  sbcreug  2941  sbcel12g  2968  sbceqg  2969  csbiebg  2992  elpwg  3465  snssg  3603  preq12bg  3647  elintg  3726  elintrabg  3731  sbcbrg  3924  opelresg  4762  elixpsn  6559  ixpsnf1o  6560  domeng  6576