Theorem vtoclbg 2916

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

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642   e. wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862

This theorem is referenced by:  pm13.183  2980  sbc8g  3054  sbc2or  3055  sbcco  3069  sbc5  3071  sbcie2g  3080  eqsbc1  3086  sbcng  3087  sbcimg  3088  sbcan  3089  sbcang  3090  sbcor  3091  sbcorg  3092  sbcbig  3093  sbcal  3094  sbcalg  3095  sbcex2  3096  sbcexg  3097  sbc3ang  3105  sbcel1gv  3106  sbcel2gv  3107  sbcralg  3121  sbcrexg  3122  sbcreug  3123  sbcel12g  3152  sbceqg  3153  csbiebg  3176  elpwg  3730  snssg  3845  elintg  3935  elintrabg  3940  preq12bg  4129  sbcbrg  4686  opbr1st  5502  opbr2nd  5503  elfix  5788  otelins2  5792  otelins3  5793  elfunsg  5831  brfns  5834