Theorem rgen2 3121

Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3159 since it depends on a smaller set of axioms. (Contributed by NM, 30-May-1999.)

Hypothesis

Ref	Expression
rgen2.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)

Assertion

Ref	Expression
rgen2	⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rgen2

Step	Hyp	Ref	Expression
1		rgen2.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)
2	1	ralrimiva 3104	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)
3	2	rgen 3075	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3070

This theorem is referenced by:  rgen3  3122  invdisjrabw  5060  invdisjrab  5061  sosn  5674  isoid  7209  f1owe  7233  epweon  7634  epweonOLD  7635  f1stres  7864  f2ndres  7865  fnwelem  7981  issmo  8188  oawordeulem  8394  ecopover  8619  unfilem2  9088  dffi2  9191  inficl  9193  fipwuni  9194  fisn  9195  dffi3  9199  cantnfvalf  9432  r111  9542  alephf1  9850  alephiso  9863  dfac5lem4  9891  kmlem9  9923  ackbij1lem17  10001  fin1a2lem2  10166  fin1a2lem4  10168  axcc2lem  10201  smobeth  10351  nqereu  10694  addpqf  10709  mulpqf  10711  genpdm  10767  axaddf  10910  axmulf  10911  subf  11232  mulnzcnopr  11630  negiso  11964  cnref1o  12734  xaddf  12967  xmulf  13015  ioof  13188  om2uzf1oi  13682  om2uzisoi  13683  wrd2ind  14445  wwlktovf1  14681  reeff1  15838  divalglem9  16119  bitsf1  16162  smupf  16194  gcdf  16228  eucalgf  16297  qredeu  16372  1arith  16637  vdwapf  16682  xpsff1o  17287  catideu  17393  sscres  17544  fpwipodrs  18267  letsr  18320  mgmidmo  18353  frmdplusg  18502  efmndmgm  18533  smndex1mgm  18555  pwmnd  18585  mulgfval  18711  nmznsg  18805  efgmf  19328  efglem  19331  efgred  19363  isabli  19410  brric  19997  xrsmgm  20642  xrs1cmn  20647  xrge0subm  20648  xrsds  20650  cnsubmlem  20655  cnsubrglem  20657  nn0srg  20677  rge0srg  20678  rzgrp  20837  fibas  22136  fctop  22163  cctop  22165  iccordt  22374  txuni2  22725  fsubbas  23027  zfbas  23056  ismeti  23487  dscmet  23737  qtopbaslem  23931  tgqioo  23972  xrsxmet  23981  xrsdsre  23982  retopconn  24001  iccconn  24002  divcn  24040  abscncf  24073  recncf  24074  imcncf  24075  cjcncf  24076  iimulcn  24110  icopnfhmeo  24115  iccpnfhmeo  24117  xrhmeo  24118  cnllycmp  24128  bndth  24130  iundisj2  24722  dyadf  24764  reefiso  25616  recosf1o  25700  cxpcn3  25910  sgmf  26303  2lgslem1b  26549  tgjustf  26843  ercgrg  26887  2wspmdisj  28710  isabloi  28922  smcnlem  29068  cncph  29190  hvsubf  29386  hhip  29548  hhph  29549  helch  29614  hsn0elch  29619  hhssabloilem  29632  hhshsslem2  29639  shscli  29688  shintcli  29700  pjmf1  30087  idunop  30349  0cnop  30350  0cnfn  30351  idcnop  30352  idhmop  30353  0hmop  30354  adj0  30365  lnophsi  30372  lnopunii  30383  lnophmi  30389  nlelshi  30431  riesz4i  30434  cnlnadjlem6  30443  cnlnadjlem9  30446  adjcoi  30471  bra11  30479  pjhmopi  30517  iundisj2f  30938  iundisj2fi  31127  xrstos  31297  xrge0omnd  31346  reofld  31553  xrge0slmod  31557  iistmd  31861  cnre2csqima  31870  mndpluscn  31885  raddcn  31888  xrge0iifiso  31894  xrge0iifmhm  31898  xrge0pluscn  31899  cnzh  31929  rezh  31930  br2base  32245  sxbrsiga  32266  signswmnd  32545  cardpred  33071  nummin  33072  indispconn  33205  cnllysconn  33216  ioosconn  33218  rellysconn  33222  fmlaomn0  33361  gonan0  33363  goaln0  33364  soseq  33812  lrcut  34092  fneref  34548  dnicn  34681  f1omptsnlem  35516  isbasisrelowl  35538  poimirlem27  35813  mblfinlem1  35823  mblfinlem2  35824  exidu1  36023  rngoideu  36070  isomliN  37260  idlaut  38117  resubf  40371  sn-subf  40417  mzpclall  40556  frmx  40742  frmy  40743  kelac2lem  40896  ontric3g  41136  clsk1indlem3  41660  icof  42766  sprsymrelf1  44959  fmtnof1  44998  prmdvdsfmtnof1  45050  uspgrsprf1  45320  plusfreseq  45337  nnsgrpmgm  45381  nnsgrp  45382  nn0mnd  45384  2zrngamgm  45508  2zrngmmgm  45515  2zrngnmrid  45519  ldepslinc  45861  rrx2xpref1o  46075  rrx2plordisom  46080  natglobalincr  46523