Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  gen2 Structured version   Visualization version   GIF version

Theorem gen2 1798
 Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
Hypothesis
Ref Expression
gen2.1 𝜑
Assertion
Ref Expression
gen2 𝑥𝑦𝜑

Proof of Theorem gen2
StepHypRef Expression
1 gen2.1 . . 3 𝜑
21ax-gen 1797 . 2 𝑦𝜑
32ax-gen 1797 1 𝑥𝑦𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1536 This theorem was proved from axioms:  ax-gen 1797 This theorem is referenced by:  axextmo  2733  moeq  3621  csbie2  3844  mosneq  4730  eusv1  5260  moop2  5361  mosubop  5370  eqrelriv  5631  opabid2  5669  xpidtr  5954  fvmptopab  7203  funoprab  7268  mpofunOLD  7271  fnoprab  7272  elovmpo  7386  wfrfun  7975  tfrlem7  8029  hartogs  9041  card2on  9051  epinid0  9097  cnvepnep  9104  tskwe  9412  ondomon  10023  fi1uzind  13907  brfi1indALT  13910  climeu  14960  letsr  17903  ulmdm  25087  wlkRes  27538  ajmoi  28740  helch  29125  hsn0elch  29130  chintcli  29213  adjmo  29714  nlelchi  29943  hmopidmchi  30033  bnj978  32449  bnj1052  32475  bnj1030  32487  funen1cnv  32585  satfv0  32836  satfv0fun  32849  fnsingle  33792  funimage  33801  funpartfun  33816  imagesset  33826  funtransport  33904  funray  34013  funline  34015  filnetlem3  34140  bj-cbvalimi  34396  bj-cbveximi  34397  ax11-pm  34573  ax11-pm2  34577  bj-snsetex  34702  wl-equsal1i  35250  mbfresfi  35405  riscer  35728  vvdifopab  35983  opabf  36082  cnvcosseq  36144  symrelcoss3  36167  cotrintab  40709  pm11.11  41473  fun2dmnopgexmpl  44230  ichv  44356  ichf  44357  ichid  44358  icht  44359  ichcircshi  44361  icheq  44369
 Copyright terms: Public domain W3C validator