Theorem rgen2 3198

Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3370 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 3145	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)
3	2	rgen 3062	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3061

This theorem is referenced by:  rgen3  3203  invdisjrab  5129  sosn  5771  isoid  7350  f1owe  7374  epweon  7796  epweonALT  7797  f1stres  8039  f2ndres  8040  fnwelem  8157  soseq  8185  issmo  8389  oawordeulem  8593  naddf  8720  ecopover  8862  unfilem2  9345  dffi2  9464  inficl  9466  fipwuni  9467  fisn  9468  dffi3  9472  cantnfvalf  9706  r111  9816  alephf1  10126  alephiso  10139  dfac5lem4  10167  dfac5lem4OLD  10169  kmlem9  10200  ackbij1lem17  10276  fin1a2lem2  10442  fin1a2lem4  10444  axcc2lem  10477  smobeth  10627  nqereu  10970  addpqf  10985  mulpqf  10987  genpdm  11043  axaddf  11186  axmulf  11187  subf  11511  mulnzcnf  11910  negiso  12249  cnref1o  13028  xaddf  13267  xmulf  13315  ioof  13488  om2uzf1oi  13995  om2uzisoi  13996  wrd2ind  14762  wwlktovf1  14997  reeff1  16157  divalglem9  16439  bitsf1  16484  smupf  16516  gcdf  16550  eucalgf  16621  qredeu  16696  1arith  16966  vdwapf  17011  xpsff1o  17613  catideu  17719  sscres  17868  fpwipodrs  18586  letsr  18639  mgmidmo  18674  frmdplusg  18868  efmndmgm  18899  smndex1mgm  18921  pwmnd  18951  mulgfval  19088  nmznsg  19187  efgmf  19732  efglem  19735  efgred  19767  isabli  19815  brric  20505  xrsmgm  21420  xrs1cmn  21425  xrge0subm  21426  xrsds  21428  cnsubmlem  21433  cnsubrglem  21435  cnsubrglemOLD  21436  nn0srg  21456  rge0srg  21457  pzriprnglem5  21497  pzriprnglem8  21500  rzgrp  21642  fibas  22985  fctop  23012  cctop  23014  iccordt  23223  txuni2  23574  fsubbas  23876  zfbas  23905  ismeti  24336  dscmet  24586  qtopbaslem  24780  tgqioo  24822  xrsxmet  24832  xrsdsre  24833  retopconn  24852  iccconn  24853  divcnOLD  24891  divcn  24893  abscncf  24928  recncf  24929  imcncf  24930  cjcncf  24931  iimulcn  24968  iimulcnOLD  24969  icopnfhmeo  24975  iccpnfhmeo  24977  xrhmeo  24978  cnllycmp  24989  bndth  24991  iundisj2  25585  dyadf  25627  reefiso  26493  recosf1o  26578  cxpcn3  26792  sgmf  27189  2lgslem1b  27437  lrcut  27942  addsf  28016  negscut  28072  negsf1o  28087  subsf  28095  mulscutlem  28158  tgjustf  28482  ercgrg  28526  2wspmdisj  30357  isabloi  30571  smcnlem  30717  cncph  30839  hvsubf  31035  hhip  31197  hhph  31198  helch  31263  hsn0elch  31268  hhssabloilem  31281  hhshsslem2  31288  shscli  31337  shintcli  31349  pjmf1  31736  idunop  31998  0cnop  31999  0cnfn  32000  idcnop  32001  idhmop  32002  0hmop  32003  adj0  32014  lnophsi  32021  lnopunii  32032  lnophmi  32038  nlelshi  32080  riesz4i  32083  cnlnadjlem6  32092  cnlnadjlem9  32095  adjcoi  32120  bra11  32128  pjhmopi  32166  iundisj2f  32604  iundisj2fi  32800  xrstos  33013  xrge0omnd  33089  reofld  33373  xrge0slmod  33377  zringfrac  33583  iistmd  33902  cnre2csqima  33911  mndpluscn  33926  raddcn  33929  xrge0iifiso  33935  xrge0iifmhm  33939  xrge0pluscn  33940  cnzh  33970  rezh  33971  br2base  34272  sxbrsiga  34293  signswmnd  34573  cardpred  35105  nummin  35106  indispconn  35240  cnllysconn  35251  ioosconn  35253  rellysconn  35257  fmlaomn0  35396  gonan0  35398  goaln0  35399  mpomulnzcnf  36301  fneref  36352  dnicn  36494  f1omptsnlem  37338  isbasisrelowl  37360  poimirlem27  37655  mblfinlem1  37665  mblfinlem2  37666  exidu1  37864  rngoideu  37911  isomliN  39241  idlaut  40099  resubf  42416  sn-subf  42463  mzpclall  42743  frmx  42930  frmy  42931  kelac2lem  43081  onsucf1o  43290  ontric3g  43540  clsk1indlem3  44061  wfaxpr  45020  icof  45229  natglobalincr  46897  sprsymrelf1  47488  fmtnof1  47527  prmdvdsfmtnof1  47579  usgrexmpl2trifr  48001  uspgrsprf1  48068  plusfreseq  48085  nnsgrpmgm  48097  nnsgrp  48098  nn0mnd  48100  2zrngamgm  48166  2zrngmmgm  48173  2zrngnmrid  48177  ldepslinc  48431  rrx2xpref1o  48644  rrx2plordisom  48649  rescofuf  48940