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

Theorem gen2 1534
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 1533 . 2  |-  A. y ph
32ax-gen 1533 1  |-  A. x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1527
This theorem is referenced by:  euequ1  2231  bm1.1  2268  vtocl3  2840  eueq  2937  csbie2  3126  moop2  4261  mosubop  4265  eusv1  4528  eqrelriv  4780  opabid2  4815  xpidtr  5065  funoprab  5944  mpt2fun  5946  fnoprab  5947  elovmpt2  6064  tfrlem7  6399  hartogs  7259  card2on  7268  tskwe  7583  ondomon  8185  climeu  12029  letsr  14349  ajmoi  21437  helch  21823  hsn0elch  21827  chintcli  21910  adjmo  22412  nlelchi  22641  hmopidmchi  22731  wfrlem11  24266  frrlem5c  24287  fnsingle  24458  funimage  24467  funpartfun  24481  funtransport  24654  funray  24763  funline  24765  filnetlem3  26329  riscer  26619  pm11.11  27570  bnj978  28981  bnj1052  29005  bnj1030  29017
This theorem was proved from axioms:  ax-gen 1533
  Copyright terms: Public domain W3C validator