Theorem rgen2 3179

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3054

This theorem is referenced by:  rgen3  3184  invdisjrab  5059  sosn  5705  isoid  7273  f1owe  7297  epweon  7718  epweonALT  7719  f1stres  7955  f2ndres  7956  fnwelem  8071  soseq  8099  issmo  8278  oawordeulem  8479  naddf  8607  ecopover  8758  unfilem2  9206  dffi2  9326  inficl  9328  fipwuni  9329  fisn  9330  dffi3  9334  cantnfvalf  9577  r111  9690  alephf1  9998  alephiso  10011  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem9  10072  ackbij1lem17  10148  fin1a2lem2  10314  fin1a2lem4  10316  axcc2lem  10349  smobeth  10500  nqereu  10843  addpqf  10858  mulpqf  10860  genpdm  10916  axaddf  11059  axmulf  11060  subf  11386  mulnzcnf  11787  negiso  12127  cnref1o  12926  xaddf  13167  xmulf  13215  ioof  13391  om2uzf1oi  13906  om2uzisoi  13907  wrd2ind  14676  wwlktovf1  14910  reeff1  16078  divalglem9  16361  bitsf1  16406  smupf  16438  gcdf  16472  eucalgf  16543  qredeu  16618  1arith  16889  vdwapf  16934  xpsff1o  17522  catideu  17632  sscres  17781  fpwipodrs  18497  letsr  18550  chninf  18592  mgmidmo  18619  frmdplusg  18813  efmndmgm  18844  smndex1mgm  18869  pwmnd  18899  mulgfval  19036  nmznsg  19134  efgmf  19679  efglem  19682  efgred  19714  isabli  19762  brric  20475  xrsmgm  21382  xrsds  21385  cnsubmlem  21390  cnsubrglem  21392  nn0srg  21412  rge0srg  21413  xrs1cmn  21417  xrge0subm  21418  xrge0omnd  21420  pzriprnglem5  21460  pzriprnglem8  21463  rzgrp  21598  fibas  22960  fctop  22987  cctop  22989  iccordt  23197  txuni2  23548  fsubbas  23850  zfbas  23879  ismeti  24308  dscmet  24555  qtopbaslem  24741  tgqioo  24783  xrsxmet  24793  xrsdsre  24794  retopconn  24813  iccconn  24814  divcn  24853  abscncf  24886  recncf  24887  imcncf  24888  cjcncf  24889  iimulcn  24923  icopnfhmeo  24928  iccpnfhmeo  24930  xrhmeo  24931  cnllycmp  24941  bndth  24943  iundisj2  25534  dyadf  25576  reefiso  26431  recosf1o  26517  cxpcn3  26730  sgmf  27126  2lgslem1b  27373  lrcut  27914  addsf  27992  negcut  28049  negsf1o  28064  subsf  28074  mulcutlem  28141  oniso  28281  bdayn0sf1o  28380  zsoring  28419  tgjustf  28559  ercgrg  28603  2wspmdisj  30425  isabloi  30640  smcnlem  30786  cncph  30908  hvsubf  31104  hhip  31266  hhph  31267  helch  31332  hsn0elch  31337  hhssabloilem  31350  hhshsslem2  31357  shscli  31406  shintcli  31418  pjmf1  31805  idunop  32067  0cnop  32068  0cnfn  32069  idcnop  32070  idhmop  32071  0hmop  32072  adj0  32083  lnophsi  32090  lnopunii  32101  lnophmi  32107  nlelshi  32149  riesz4i  32152  cnlnadjlem6  32161  cnlnadjlem9  32164  adjcoi  32189  bra11  32197  pjhmopi  32235  iundisj2f  32679  iundisj2fi  32889  xrstos  33089  reofld  33426  xrge0slmod  33431  zringfrac  33637  iistmd  34086  cnre2csqima  34095  mndpluscn  34110  raddcn  34113  xrge0iifiso  34119  xrge0iifmhm  34123  xrge0pluscn  34124  cnzh  34152  rezh  34153  br2base  34453  sxbrsiga  34474  signswmnd  34741  cardpred  35273  nummin  35274  indispconn  35462  cnllysconn  35473  ioosconn  35475  rellysconn  35479  fmlaomn0  35618  gonan0  35620  goaln0  35621  mpomulnzcnf  36527  fneref  36578  dnicn  36798  f1omptsnlem  37698  isbasisrelowl  37720  poimirlem27  38014  mblfinlem1  38024  mblfinlem2  38025  exidu1  38223  rngoideu  38270  isomliN  39731  idlaut  40588  resubf  42858  sn-subf  42906  mzpclall  43176  frmx  43358  frmy  43359  kelac2lem  43509  onsucf1o  43717  ontric3g  43966  clsk1indlem3  44487  wfaxpr  45442  icof  45664  natglobalincr  47322  sprsymrelf1  47971  fmtnof1  48013  prmdvdsfmtnof1  48065  usgrexmpl2trifr  48528  uspgrsprf1  48638  plusfreseq  48655  nnsgrpmgm  48667  nnsgrp  48668  nn0mnd  48670  2zrngamgm  48736  2zrngmmgm  48743  2zrngnmrid  48747  ldepslinc  49000  rrx2xpref1o  49209  rrx2plordisom  49214  rescofuf  49583  oppff1  49638