MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclbg Structured version   Unicode version

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
StepHypRef Expression
1 vtoclbg.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
2 vtoclbg.2 . . 3  |-  ( x  =  A  ->  ( ps 
<->  th ) )
31, 2bibi12d 321 . 2  |-  ( x  =  A  ->  (
( ph  <->  ps )  <->  ( ch  <->  th ) ) )
4 vtoclbg.3 . 2  |-  ( ph  <->  ps )
53, 4vtoclg 3153 1  |-  ( A  e.  V  ->  ( ch 
<->  th ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator