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

Theorem gen2 1799
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 1798 . 2 𝑦𝜑
32ax-gen 1798 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1540
This theorem was proved from axioms:  ax-gen 1798
This theorem is referenced by:  axextmo  2708  moeq  3703  csbie2  3935  mosneq  4843  eusv1  5389  moop2  5502  mosubop  5511  eqrelriv  5788  opabid2  5827  xpidtr  6121  fvmptopabOLD  7461  funoprab  7527  mpofunOLD  7530  fnoprab  7531  elovmpo  7648  wfrfunOLD  8316  tfrlem7  8380  hartogs  9536  card2on  9546  epinid0  9592  cnvepnep  9600  ssttrcl  9707  tskwe  9942  ondomon  10555  fi1uzind  14455  brfi1indALT  14458  climeu  15496  letsr  18543  ulmdm  25897  wlkResOLD  28897  ajmoi  30099  helch  30484  hsn0elch  30489  chintcli  30572  adjmo  31073  nlelchi  31302  hmopidmchi  31392  bnj978  33949  bnj1052  33975  bnj1030  33987  funen1cnv  34080  satfv0  34338  satfv0fun  34351  fnsingle  34880  funimage  34889  funpartfun  34904  imagesset  34914  funtransport  34992  funray  35101  funline  35103  filnetlem3  35254  bj-cbvalimi  35513  bj-cbveximi  35514  ax11-pm  35699  ax11-pm2  35703  bj-snsetex  35833  wl-equsal1i  36401  mbfresfi  36523  riscer  36845  vvdifopab  37117  opabf  37226  cnvcosseq  37296  antisymressn  37303  trressn  37304  symrelcoss3  37324  cotrintab  42351  pm11.11  43119  fun2dmnopgexmpl  45979  ichv  46104  ichf  46105  ichid  46106  icht  46107  ichcircshi  46109  icheq  46117  mof0ALT  47460  f1omo  47481
  Copyright terms: Public domain W3C validator