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

Theorem gen2 1871
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 1870 . 2 𝑦𝜑
32ax-gen 1870 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1629
This theorem was proved from axioms:  ax-gen 1870
This theorem is referenced by:  bm1.1  2756  vtocl3  3413  eueq  3530  csbie2  3712  eusv1  4991  moop2  5093  mosubop  5104  eqrelriv  5351  opabid2  5388  xpidtr  5657  fvmptopab  6842  funoprab  6905  mpt2fun  6907  fnoprab  6908  elovmpt2  7024  wfrfun  7576  tfrlem7  7630  hartogs  8603  card2on  8613  epinid0  8659  cnvepnep  8665  tskwe  8974  ondomon  9585  fi1uzind  13474  brfi1indALT  13477  climeu  14487  letsr  17428  ulmdm  24360  wlkRes  26774  ajmoi  28047  helch  28433  hsn0elch  28438  chintcli  28523  adjmo  29024  nlelchi  29253  hmopidmchi  29343  bnj978  31350  bnj1052  31374  bnj1030  31386  frrlem5c  32116  fnsingle  32356  funimage  32365  funpartfun  32380  imagesset  32390  funtransport  32468  funray  32577  funline  32579  filnetlem3  32705  ax11-pm  33147  ax11-pm2  33151  bj-dfclel  33211  bj-dfcleq  33216  bj-snsetex  33275  wl-equsal1i  33657  mbfresfi  33781  riscer  34112  vvdifopab  34360  opabf  34465  cnvcosseq  34527  symrelcoss3  34550  cotrintab  38440  pm11.11  39092  fun2dmnopgexmpl  41819
  Copyright terms: Public domain W3C validator