Theorem rgen2 3176

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  rgen3  3181  invdisjrab  5085  sosn  5711  isoid  7275  f1owe  7299  epweon  7720  epweonALT  7721  f1stres  7957  f2ndres  7958  fnwelem  8073  soseq  8101  issmo  8280  oawordeulem  8481  naddf  8609  ecopover  8758  unfilem2  9206  dffi2  9326  inficl  9328  fipwuni  9329  fisn  9330  dffi3  9334  cantnfvalf  9574  r111  9687  alephf1  9995  alephiso  10008  dfac5lem4  10036  dfac5lem4OLD  10038  kmlem9  10069  ackbij1lem17  10145  fin1a2lem2  10311  fin1a2lem4  10313  axcc2lem  10346  smobeth  10497  nqereu  10840  addpqf  10855  mulpqf  10857  genpdm  10913  axaddf  11056  axmulf  11057  subf  11382  mulnzcnf  11783  negiso  12122  cnref1o  12898  xaddf  13139  xmulf  13187  ioof  13363  om2uzf1oi  13876  om2uzisoi  13877  wrd2ind  14646  wwlktovf1  14880  reeff1  16045  divalglem9  16328  bitsf1  16373  smupf  16405  gcdf  16439  eucalgf  16510  qredeu  16585  1arith  16855  vdwapf  16900  xpsff1o  17488  catideu  17598  sscres  17747  fpwipodrs  18463  letsr  18516  chninf  18558  mgmidmo  18585  frmdplusg  18779  efmndmgm  18810  smndex1mgm  18832  pwmnd  18862  mulgfval  18999  nmznsg  19097  efgmf  19642  efglem  19645  efgred  19677  isabli  19725  brric  20437  xrsmgm  21361  xrsds  21364  cnsubmlem  21369  cnsubrglem  21371  cnsubrglemOLD  21372  nn0srg  21392  rge0srg  21393  xrs1cmn  21397  xrge0subm  21398  xrge0omnd  21400  pzriprnglem5  21440  pzriprnglem8  21443  rzgrp  21578  fibas  22921  fctop  22948  cctop  22950  iccordt  23158  txuni2  23509  fsubbas  23811  zfbas  23840  ismeti  24269  dscmet  24516  qtopbaslem  24702  tgqioo  24744  xrsxmet  24754  xrsdsre  24755  retopconn  24774  iccconn  24775  divcnOLD  24813  divcn  24815  abscncf  24850  recncf  24851  imcncf  24852  cjcncf  24853  iimulcn  24890  iimulcnOLD  24891  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  cnllycmp  24911  bndth  24913  iundisj2  25506  dyadf  25548  reefiso  26414  recosf1o  26500  cxpcn3  26714  sgmf  27111  2lgslem1b  27359  lrcut  27900  addsf  27978  negcut  28035  negsf1o  28050  subsf  28060  mulcutlem  28127  oniso  28267  bdayn0sf1o  28366  zsoring  28405  tgjustf  28545  ercgrg  28589  2wspmdisj  30412  isabloi  30626  smcnlem  30772  cncph  30894  hvsubf  31090  hhip  31252  hhph  31253  helch  31318  hsn0elch  31323  hhssabloilem  31336  hhshsslem2  31343  shscli  31392  shintcli  31404  pjmf1  31791  idunop  32053  0cnop  32054  0cnfn  32055  idcnop  32056  idhmop  32057  0hmop  32058  adj0  32069  lnophsi  32076  lnopunii  32087  lnophmi  32093  nlelshi  32135  riesz4i  32138  cnlnadjlem6  32147  cnlnadjlem9  32150  adjcoi  32175  bra11  32183  pjhmopi  32221  iundisj2f  32665  iundisj2fi  32877  xrstos  33092  reofld  33424  xrge0slmod  33429  zringfrac  33635  iistmd  34059  cnre2csqima  34068  mndpluscn  34083  raddcn  34086  xrge0iifiso  34092  xrge0iifmhm  34096  xrge0pluscn  34097  cnzh  34125  rezh  34126  br2base  34426  sxbrsiga  34447  signswmnd  34714  cardpred  35248  nummin  35249  indispconn  35428  cnllysconn  35439  ioosconn  35441  rellysconn  35445  fmlaomn0  35584  gonan0  35586  goaln0  35587  mpomulnzcnf  36493  fneref  36544  dnicn  36692  f1omptsnlem  37541  isbasisrelowl  37563  poimirlem27  37848  mblfinlem1  37858  mblfinlem2  37859  exidu1  38057  rngoideu  38104  isomliN  39499  idlaut  40356  resubf  42636  sn-subf  42684  mzpclall  42969  frmx  43155  frmy  43156  kelac2lem  43306  onsucf1o  43514  ontric3g  43763  clsk1indlem3  44284  wfaxpr  45239  icof  45463  natglobalincr  47121  sprsymrelf1  47742  fmtnof1  47781  prmdvdsfmtnof1  47833  usgrexmpl2trifr  48283  uspgrsprf1  48393  plusfreseq  48410  nnsgrpmgm  48422  nnsgrp  48423  nn0mnd  48425  2zrngamgm  48491  2zrngmmgm  48498  2zrngnmrid  48502  ldepslinc  48755  rrx2xpref1o  48964  rrx2plordisom  48969  rescofuf  49338  oppff1  49393