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

Theorem gen2 1619
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 1618 . 2
32ax-gen 1618 1
Colors of variables: wff setvar class
Syntax hints:  A.wal 1393
This theorem is referenced by:  euequ1OLD  2387  bm1.1  2440  bm1.1OLD  2441  vtocl3  3163  eueq  3271  csbie2  3464  eusv1  4646  moop2  4747  mosubop  4751  eqrelriv  5101  opabid2  5137  xpidtr  5394  funoprab  6402  mpt2fun  6404  fnoprab  6405  elovmpt2  6520  tfrlem7  7071  hartogs  7990  card2on  8001  tskwe  8352  ondomon  8959  brfi1uzind  12532  climeu  13378  letsr  15857  ulmdm  22788  wlkres  24522  crcts  24622  cycls  24623  ajmoi  25774  helch  26161  hsn0elch  26166  chintcli  26249  adjmo  26751  nlelchi  26980  hmopidmchi  27070  wfrlem11  29353  frrlem5c  29393  fnsingle  29569  funimage  29578  funpartfun  29593  imagesset  29603  funtransport  29681  funray  29790  funline  29792  wl-equsal1i  29996  mbfresfi  30061  filnetlem3  30198  riscer  30391  pm11.11  31279  bnj978  34007  bnj1052  34031  bnj1030  34043  ax11-pm  34405  ax11-pm2  34409  bj-snsetex  34521
This theorem was proved from axioms:  ax-gen 1618
  Copyright terms: Public domain W3C validator