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

Theorem vtoclbg 3168
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)
Hypotheses
Ref Expression
vtoclbg.1
vtoclbg.2
vtoclbg.3
Assertion
Ref Expression
vtoclbg
Distinct variable groups:   ,   ,   ,

Proof of Theorem vtoclbg
StepHypRef Expression
1 vtoclbg.1 . . 3
2 vtoclbg.2 . . 3
31, 2bibi12d 321 . 2
4 vtoclbg.3 . 2
53, 4vtoclg 3167 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818
This theorem is referenced by:  alexeqg  3228  pm13.183  3240  sbc8g  3335  sbc2or  3336  sbcco  3350  sbc5  3352  sbcie2g  3361  eqsbc3  3367  sbcng  3368  sbcimg  3369  sbcan  3370  sbcangOLD  3371  sbcor  3372  sbcorgOLD  3373  sbcbig  3374  sbcal  3379  sbcalgOLD  3380  sbcex2  3381  sbcexgOLD  3382  sbc3angOLD  3391  sbcel1v  3392  sbcel1gvOLD  3393  sbcrexgOLD  3413  sbcreu  3414  sbcreugOLD  3415  csbiebg  3457  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  elpwg  4020  snssg  4163  preq12bg  4209  elintg  4294  elintrabg  4299  sbcbr123  4503  sbcbrgOLD  4504  opelresg  5286  funfvima3  6149  elixpsn  7528  ixpsnf1o  7529  domeng  7550  1sdom  7742  rankcf  9176  pt1hmeo  20307  eldm3  29191  elima4  29209  brsset  29539  brbigcup  29548  elfix2  29554  elfunsg  29566  elsingles  29568  funpartlem  29592  ellines  29802  elhf2g  29833  cover2g  30205  inisegn0  30989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator