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

Theorem vtoclbg 3146
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 322 . 2  |-  ( x  =  A  ->  (
( ph  <->  ps )  <->  ( ch  <->  th ) ) )
4 vtoclbg.3 . 2  |-  ( ph  <->  ps )
53, 4vtoclg 3145 1  |-  ( A  e.  V  ->  ( ch 
<->  th ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-v 3089
This theorem is referenced by:  alexeqg  3206  pm13.183  3218  sbc8g  3313  sbc2or  3314  sbcco  3328  sbc5  3330  sbcie2g  3339  eqsbc3  3345  sbcng  3346  sbcimg  3347  sbcan  3348  sbcor  3349  sbcbig  3350  sbcal  3355  sbcex2  3356  sbcel1v  3364  sbcreu  3382  csbiebg  3424  sbcel12  3806  sbceqg  3807  elpwg  3993  snssg  4136  preq12bg  4182  elintg  4266  elintrabg  4271  sbcbr123  4477  opelresg  5132  inisegn0  5220  funfvima3  6157  elixpsn  7569  ixpsnf1o  7570  domeng  7591  1sdom  7781  rankcf  9201  pt1hmeo  20752  eldm3  30189  br1steqg  30203  br2ndeqg  30204  elima4  30208  brsset  30441  brbigcup  30450  elfix2  30456  elfunsg  30468  elsingles  30470  funpartlem  30494  ellines  30704  elhf2g  30728  cover2g  31744  sbcrexgOLD  35336  sbcangOLD  36526  sbcorgOLD  36527  sbcalgOLD  36539  sbcexgOLD  36540  sbcel12gOLD  36541  sbcel1gvOLD  36894
  Copyright terms: Public domain W3C validator