Theorem vtoclbg 2787

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728

This theorem is referenced by:  pm13.183  2864  sbc8g  2958  sbcco  2972  sbc5  2974  sbcie2g  2984  eqsbc1  2990  sbcng  2991  sbcimg  2992  sbcan  2993  sbcang  2994  sbcor  2995  sbcorg  2996  sbcbig  2997  sbcal  3002  sbcalg  3003  sbcex2  3004  sbcexg  3005  sbcel1v  3013  sbcralg  3029  sbcreug  3031  sbcel12g  3060  sbceqg  3061  csbiebg  3087  elpwg  3567  snssg  3709  preq12bg  3753  elintg  3832  elintrabg  3837  sbcbrg  4036  opelresg  4891  elixpsn  6701  ixpsnf1o  6702  domeng  6718