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  2794  moeq  3695  csbie2  3919  mosneq  4765  eusv1  5282  moop2  5383  mosubop  5392  eqrelriv  5655  opabid2  5693  xpidtr  5975  fvmptopab  7198  funoprab  7263  mpofun  7265  fnoprab  7266  elovmpo  7379  wfrfun  7954  tfrlem7  8008  hartogs  8996  card2on  9006  epinid0  9052  cnvepnep  9059  tskwe  9367  ondomon  9973  fi1uzind  13843  brfi1indALT  13846  climeu  14900  letsr  17825  ulmdm  24908  wlkRes  27358  ajmoi  28562  helch  28947  hsn0elch  28952  chintcli  29035  adjmo  29536  nlelchi  29765  hmopidmchi  29855  bnj978  32120  bnj1052  32144  bnj1030  32156  funen1cnv  32254  satfv0  32502  satfv0fun  32515  fnsingle  33277  funimage  33286  funpartfun  33301  imagesset  33311  funtransport  33389  funray  33498  funline  33500  filnetlem3  33625  bj-cbvalimi  33877  bj-cbveximi  33878  ax11-pm  34052  ax11-pm2  34056  bj-snsetex  34172  wl-equsal1i  34664  mbfresfi  34819  riscer  35147  vvdifopab  35402  opabf  35500  cnvcosseq  35562  symrelcoss3  35585  cotrintab  39852  pm11.11  40583  fun2dmnopgexmpl  43360  ichv  43486  ichf  43487  ichid  43488  ichcircshi  43489  icheq  43497
  Copyright terms: Public domain W3C validator