Theorem rgen2 3178

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  rgen3  3183  invdisjrab  5073  sosn  5711  isoid  7277  f1owe  7301  epweon  7722  epweonALT  7723  f1stres  7959  f2ndres  7960  fnwelem  8074  soseq  8102  issmo  8281  oawordeulem  8482  naddf  8610  ecopover  8761  unfilem2  9209  dffi2  9329  inficl  9331  fipwuni  9332  fisn  9333  dffi3  9337  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  20472  xrsmgm  21396  xrsds  21399  cnsubmlem  21404  cnsubrglem  21406  cnsubrglemOLD  21407  nn0srg  21427  rge0srg  21428  xrs1cmn  21432  xrge0subm  21433  xrge0omnd  21435  pzriprnglem5  21475  pzriprnglem8  21478  rzgrp  21613  fibas  22952  fctop  22979  cctop  22981  iccordt  23189  txuni2  23540  fsubbas  23842  zfbas  23871  ismeti  24300  dscmet  24547  qtopbaslem  24733  tgqioo  24775  xrsxmet  24785  xrsdsre  24786  retopconn  24805  iccconn  24806  divcn  24845  abscncf  24878  recncf  24879  imcncf  24880  cjcncf  24881  iimulcn  24915  icopnfhmeo  24920  iccpnfhmeo  24922  xrhmeo  24923  cnllycmp  24933  bndth  24935  iundisj2  25526  dyadf  25568  reefiso  26426  recosf1o  26512  cxpcn3  26725  sgmf  27122  2lgslem1b  27369  lrcut  27910  addsf  27988  negcut  28045  negsf1o  28060  subsf  28070  mulcutlem  28137  oniso  28277  bdayn0sf1o  28376  zsoring  28415  tgjustf  28555  ercgrg  28599  2wspmdisj  30422  isabloi  30637  smcnlem  30783  cncph  30905  hvsubf  31101  hhip  31263  hhph  31264  helch  31329  hsn0elch  31334  hhssabloilem  31347  hhshsslem2  31354  shscli  31403  shintcli  31415  pjmf1  31802  idunop  32064  0cnop  32065  0cnfn  32066  idcnop  32067  idhmop  32068  0hmop  32069  adj0  32080  lnophsi  32087  lnopunii  32098  lnophmi  32104  nlelshi  32146  riesz4i  32149  cnlnadjlem6  32158  cnlnadjlem9  32161  adjcoi  32186  bra11  32194  pjhmopi  32232  iundisj2f  32675  iundisj2fi  32885  xrstos  33085  reofld  33418  xrge0slmod  33423  zringfrac  33629  iistmd  34062  cnre2csqima  34071  mndpluscn  34086  raddcn  34089  xrge0iifiso  34095  xrge0iifmhm  34099  xrge0pluscn  34100  cnzh  34128  rezh  34129  br2base  34429  sxbrsiga  34450  signswmnd  34717  cardpred  35251  nummin  35252  indispconn  35432  cnllysconn  35443  ioosconn  35445  rellysconn  35449  fmlaomn0  35588  gonan0  35590  goaln0  35591  mpomulnzcnf  36497  fneref  36548  dnicn  36768  f1omptsnlem  37666  isbasisrelowl  37688  poimirlem27  37982  mblfinlem1  37992  mblfinlem2  37993  exidu1  38191  rngoideu  38238  isomliN  39699  idlaut  40556  resubf  42827  sn-subf  42875  mzpclall  43173  frmx  43359  frmy  43360  kelac2lem  43510  onsucf1o  43718  ontric3g  43967  clsk1indlem3  44488  wfaxpr  45443  icof  45666  natglobalincr  47323  sprsymrelf1  47968  fmtnof1  48010  prmdvdsfmtnof1  48062  usgrexmpl2trifr  48525  uspgrsprf1  48635  plusfreseq  48652  nnsgrpmgm  48664  nnsgrp  48665  nn0mnd  48667  2zrngamgm  48733  2zrngmmgm  48740  2zrngnmrid  48744  ldepslinc  48997  rrx2xpref1o  49206  rrx2plordisom  49211  rescofuf  49580  oppff1  49635