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

Theorem gen2 1790
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 1789 . 2 𝑦𝜑
32ax-gen 1789 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1528
This theorem was proved from axioms:  ax-gen 1789
This theorem is referenced by:  axextmo  2802  moeq  3702  csbie2  3926  mosneq  4772  eusv1  5288  moop2  5389  mosubop  5398  eqrelriv  5661  opabid2  5699  xpidtr  5981  fvmptopab  7203  funoprab  7268  mpofun  7270  fnoprab  7271  elovmpo  7384  wfrfun  7961  tfrlem7  8015  hartogs  9002  card2on  9012  epinid0  9058  cnvepnep  9065  tskwe  9373  ondomon  9979  fi1uzind  13850  brfi1indALT  13853  climeu  14907  letsr  17832  ulmdm  24915  wlkRes  27364  ajmoi  28568  helch  28953  hsn0elch  28958  chintcli  29041  adjmo  29542  nlelchi  29771  hmopidmchi  29861  bnj978  32126  bnj1052  32150  bnj1030  32162  funen1cnv  32260  satfv0  32508  satfv0fun  32521  fnsingle  33283  funimage  33292  funpartfun  33307  imagesset  33317  funtransport  33395  funray  33504  funline  33506  filnetlem3  33631  bj-cbvalimi  33883  bj-cbveximi  33884  ax11-pm  34058  ax11-pm2  34062  bj-snsetex  34178  wl-equsal1i  34670  mbfresfi  34824  riscer  35153  vvdifopab  35408  opabf  35506  cnvcosseq  35568  symrelcoss3  35591  cotrintab  39858  pm11.11  40590  fun2dmnopgexmpl  43368  ichv  43460  ichf  43461  ichid  43462  ichcircshi  43463  icheq  43471
  Copyright terms: Public domain W3C validator