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

Theorem gen2 1537
Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
Hypothesis
Ref Expression
gen2.1  |-  ph
Assertion
Ref Expression
gen2  |-  A. x A. y ph

Proof of Theorem gen2
StepHypRef Expression
1 gen2.1 . . 3  |-  ph
21ax-gen 1536 . 2  |-  A. y ph
32ax-gen 1536 1  |-  A. x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1530
This theorem is referenced by:  euequ1  2244  bm1.1  2281  vtocl3  2853  eueq  2950  csbie2  3139  moop2  4277  mosubop  4281  eusv1  4544  eqrelriv  4796  opabid2  4831  xpidtr  5081  funoprab  5960  mpt2fun  5962  fnoprab  5963  elovmpt2  6080  tfrlem7  6415  hartogs  7275  card2on  7284  tskwe  7599  ondomon  8201  climeu  12045  letsr  14365  ajmoi  21453  helch  21839  hsn0elch  21843  chintcli  21926  adjmo  22428  nlelchi  22657  hmopidmchi  22747  wfrlem11  24337  frrlem5c  24358  fnsingle  24529  funimage  24538  funpartfun  24553  funtransport  24726  funray  24835  funline  24837  filnetlem3  26432  riscer  26722  pm11.11  27673  bnj978  29297  bnj1052  29321  bnj1030  29333
This theorem was proved from axioms:  ax-gen 1536
  Copyright terms: Public domain W3C validator