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

Theorem gen2 1788
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 1787 . 2 𝑦𝜑
32ax-gen 1787 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1526
This theorem was proved from axioms:  ax-gen 1787
This theorem is referenced by:  axextmo  2797  moeq  3697  csbie2  3921  mosneq  4767  eusv1  5283  moop2  5384  mosubop  5393  eqrelriv  5656  opabid2  5694  xpidtr  5976  fvmptopab  7198  funoprab  7263  mpofun  7265  fnoprab  7266  elovmpo  7379  wfrfun  7956  tfrlem7  8010  hartogs  8997  card2on  9007  epinid0  9053  cnvepnep  9060  tskwe  9368  ondomon  9974  fi1uzind  13845  brfi1indALT  13848  climeu  14902  letsr  17827  ulmdm  24910  wlkRes  27359  ajmoi  28563  helch  28948  hsn0elch  28953  chintcli  29036  adjmo  29537  nlelchi  29766  hmopidmchi  29856  bnj978  32121  bnj1052  32145  bnj1030  32157  funen1cnv  32255  satfv0  32503  satfv0fun  32516  fnsingle  33278  funimage  33287  funpartfun  33302  imagesset  33312  funtransport  33390  funray  33499  funline  33501  filnetlem3  33626  bj-cbvalimi  33878  bj-cbveximi  33879  ax11-pm  34053  ax11-pm2  34057  bj-snsetex  34173  wl-equsal1i  34665  mbfresfi  34820  riscer  35149  vvdifopab  35404  opabf  35502  cnvcosseq  35564  symrelcoss3  35587  cotrintab  39854  pm11.11  40586  fun2dmnopgexmpl  43364  ichv  43456  ichf  43457  ichid  43458  ichcircshi  43459  icheq  43467
  Copyright terms: Public domain W3C validator