Theorem rgen2 3205

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067

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

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

This theorem is referenced by:  rgen3  3210  invdisjrab  5153  sosn  5786  isoid  7365  f1owe  7389  epweon  7810  epweonALT  7811  f1stres  8054  f2ndres  8055  fnwelem  8172  soseq  8200  issmo  8404  oawordeulem  8610  naddf  8737  ecopover  8879  unfilem2  9372  dffi2  9492  inficl  9494  fipwuni  9495  fisn  9496  dffi3  9500  cantnfvalf  9734  r111  9844  alephf1  10154  alephiso  10167  dfac5lem4  10195  dfac5lem4OLD  10197  kmlem9  10228  ackbij1lem17  10304  fin1a2lem2  10470  fin1a2lem4  10472  axcc2lem  10505  smobeth  10655  nqereu  10998  addpqf  11013  mulpqf  11015  genpdm  11071  axaddf  11214  axmulf  11215  subf  11538  mulnzcnf  11936  negiso  12275  cnref1o  13050  xaddf  13286  xmulf  13334  ioof  13507  om2uzf1oi  14004  om2uzisoi  14005  wrd2ind  14771  wwlktovf1  15006  reeff1  16168  divalglem9  16449  bitsf1  16492  smupf  16524  gcdf  16558  eucalgf  16630  qredeu  16705  1arith  16974  vdwapf  17019  xpsff1o  17627  catideu  17733  sscres  17884  fpwipodrs  18610  letsr  18663  mgmidmo  18698  frmdplusg  18889  efmndmgm  18920  smndex1mgm  18942  pwmnd  18972  mulgfval  19109  nmznsg  19208  efgmf  19755  efglem  19758  efgred  19790  isabli  19838  brric  20530  xrsmgm  21442  xrs1cmn  21447  xrge0subm  21448  xrsds  21450  cnsubmlem  21455  cnsubrglem  21457  cnsubrglemOLD  21458  nn0srg  21478  rge0srg  21479  pzriprnglem5  21519  pzriprnglem8  21522  rzgrp  21664  fibas  23005  fctop  23032  cctop  23034  iccordt  23243  txuni2  23594  fsubbas  23896  zfbas  23925  ismeti  24356  dscmet  24606  qtopbaslem  24800  tgqioo  24841  xrsxmet  24850  xrsdsre  24851  retopconn  24870  iccconn  24871  divcnOLD  24909  divcn  24911  abscncf  24946  recncf  24947  imcncf  24948  cjcncf  24949  iimulcn  24986  iimulcnOLD  24987  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  cnllycmp  25007  bndth  25009  iundisj2  25603  dyadf  25645  reefiso  26510  recosf1o  26595  cxpcn3  26809  sgmf  27206  2lgslem1b  27454  lrcut  27959  addsf  28033  negscut  28089  negsf1o  28104  subsf  28112  mulscutlem  28175  tgjustf  28499  ercgrg  28543  2wspmdisj  30369  isabloi  30583  smcnlem  30729  cncph  30851  hvsubf  31047  hhip  31209  hhph  31210  helch  31275  hsn0elch  31280  hhssabloilem  31293  hhshsslem2  31300  shscli  31349  shintcli  31361  pjmf1  31748  idunop  32010  0cnop  32011  0cnfn  32012  idcnop  32013  idhmop  32014  0hmop  32015  adj0  32026  lnophsi  32033  lnopunii  32044  lnophmi  32050  nlelshi  32092  riesz4i  32095  cnlnadjlem6  32104  cnlnadjlem9  32107  adjcoi  32132  bra11  32140  pjhmopi  32178  iundisj2f  32612  iundisj2fi  32802  xrstos  32993  xrge0omnd  33061  reofld  33337  xrge0slmod  33341  zringfrac  33547  iistmd  33848  cnre2csqima  33857  mndpluscn  33872  raddcn  33875  xrge0iifiso  33881  xrge0iifmhm  33885  xrge0pluscn  33886  cnzh  33916  rezh  33917  br2base  34234  sxbrsiga  34255  signswmnd  34534  cardpred  35066  nummin  35067  indispconn  35202  cnllysconn  35213  ioosconn  35215  rellysconn  35219  fmlaomn0  35358  gonan0  35360  goaln0  35361  mpomulnzcnf  36265  fneref  36316  dnicn  36458  f1omptsnlem  37302  isbasisrelowl  37324  poimirlem27  37607  mblfinlem1  37617  mblfinlem2  37618  exidu1  37816  rngoideu  37863  isomliN  39195  idlaut  40053  resubf  42357  sn-subf  42404  mzpclall  42683  frmx  42870  frmy  42871  kelac2lem  43021  onsucf1o  43234  ontric3g  43484  clsk1indlem3  44005  icof  45126  natglobalincr  46796  sprsymrelf1  47370  fmtnof1  47409  prmdvdsfmtnof1  47461  usgrexmpl2trifr  47852  uspgrsprf1  47870  plusfreseq  47887  nnsgrpmgm  47899  nnsgrp  47900  nn0mnd  47902  2zrngamgm  47968  2zrngmmgm  47975  2zrngnmrid  47979  ldepslinc  48238  rrx2xpref1o  48452  rrx2plordisom  48457