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

Theorem gen2 1720
 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 1719 . 2 𝑦𝜑
32ax-gen 1719 1 𝑥𝑦𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1478 This theorem was proved from axioms:  ax-gen 1719 This theorem is referenced by:  bm1.1  2606  vtocl3  3251  eueq  3364  csbie2  3548  eusv1  4825  moop2  4931  mosubop  4938  eqrelriv  5179  opabid2  5216  xpidtr  5482  fvmptopab  6657  funoprab  6720  mpt2fun  6722  fnoprab  6723  elovmpt2  6839  wfrfun  7377  tfrlem7  7431  hartogs  8400  card2on  8410  tskwe  8727  ondomon  9336  fi1uzind  13225  brfi1indALT  13228  fi1uzindOLD  13231  brfi1indALTOLD  13234  climeu  14227  letsr  17155  ulmdm  24064  wlkRes  26428  ajmoi  27581  helch  27967  hsn0elch  27972  chintcli  28057  adjmo  28558  nlelchi  28787  hmopidmchi  28877  bnj978  30754  bnj1052  30778  bnj1030  30790  frrlem5c  31514  fnsingle  31695  funimage  31704  funpartfun  31719  imagesset  31729  funtransport  31807  funray  31916  funline  31918  filnetlem3  32044  ax11-pm  32489  ax11-pm2  32493  bj-dfclel  32563  bj-dfcleq  32568  bj-snsetex  32625  wl-equsal1i  32988  mbfresfi  33115  riscer  33446  cotrintab  37429  pm11.11  38082  fun2dmnopgexmpl  40621
 Copyright terms: Public domain W3C validator