Theorem rgen2 3178

Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3343 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  5087  sosn  5719  isoid  7285  f1owe  7309  epweon  7730  epweonALT  7731  f1stres  7967  f2ndres  7968  fnwelem  8083  soseq  8111  issmo  8290  oawordeulem  8491  naddf  8619  ecopover  8770  unfilem2  9218  dffi2  9338  inficl  9340  fipwuni  9341  fisn  9342  dffi3  9346  cantnfvalf  9586  r111  9699  alephf1  10007  alephiso  10020  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem9  10081  ackbij1lem17  10157  fin1a2lem2  10323  fin1a2lem4  10325  axcc2lem  10358  smobeth  10509  nqereu  10852  addpqf  10867  mulpqf  10869  genpdm  10925  axaddf  11068  axmulf  11069  subf  11394  mulnzcnf  11795  negiso  12134  cnref1o  12910  xaddf  13151  xmulf  13199  ioof  13375  om2uzf1oi  13888  om2uzisoi  13889  wrd2ind  14658  wwlktovf1  14892  reeff1  16057  divalglem9  16340  bitsf1  16385  smupf  16417  gcdf  16451  eucalgf  16522  qredeu  16597  1arith  16867  vdwapf  16912  xpsff1o  17500  catideu  17610  sscres  17759  fpwipodrs  18475  letsr  18528  chninf  18570  mgmidmo  18597  frmdplusg  18791  efmndmgm  18822  smndex1mgm  18844  pwmnd  18874  mulgfval  19011  nmznsg  19109  efgmf  19654  efglem  19657  efgred  19689  isabli  19737  brric  20449  xrsmgm  21373  xrsds  21376  cnsubmlem  21381  cnsubrglem  21383  cnsubrglemOLD  21384  nn0srg  21404  rge0srg  21405  xrs1cmn  21409  xrge0subm  21410  xrge0omnd  21412  pzriprnglem5  21452  pzriprnglem8  21455  rzgrp  21590  fibas  22933  fctop  22960  cctop  22962  iccordt  23170  txuni2  23521  fsubbas  23823  zfbas  23852  ismeti  24281  dscmet  24528  qtopbaslem  24714  tgqioo  24756  xrsxmet  24766  xrsdsre  24767  retopconn  24786  iccconn  24787  divcnOLD  24825  divcn  24827  abscncf  24862  recncf  24863  imcncf  24864  cjcncf  24865  iimulcn  24902  iimulcnOLD  24903  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  cnllycmp  24923  bndth  24925  iundisj2  25518  dyadf  25560  reefiso  26426  recosf1o  26512  cxpcn3  26726  sgmf  27123  2lgslem1b  27371  lrcut  27912  addsf  27990  negcut  28047  negsf1o  28062  subsf  28072  mulcutlem  28139  oniso  28279  bdayn0sf1o  28378  zsoring  28417  tgjustf  28557  ercgrg  28601  2wspmdisj  30424  isabloi  30639  smcnlem  30785  cncph  30907  hvsubf  31103  hhip  31265  hhph  31266  helch  31331  hsn0elch  31336  hhssabloilem  31349  hhshsslem2  31356  shscli  31405  shintcli  31417  pjmf1  31804  idunop  32066  0cnop  32067  0cnfn  32068  idcnop  32069  idhmop  32070  0hmop  32071  adj0  32082  lnophsi  32089  lnopunii  32100  lnophmi  32106  nlelshi  32148  riesz4i  32151  cnlnadjlem6  32160  cnlnadjlem9  32163  adjcoi  32188  bra11  32196  pjhmopi  32234  iundisj2f  32677  iundisj2fi  32888  xrstos  33103  reofld  33436  xrge0slmod  33441  zringfrac  33647  iistmd  34080  cnre2csqima  34089  mndpluscn  34104  raddcn  34107  xrge0iifiso  34113  xrge0iifmhm  34117  xrge0pluscn  34118  cnzh  34146  rezh  34147  br2base  34447  sxbrsiga  34468  signswmnd  34735  cardpred  35269  nummin  35270  indispconn  35450  cnllysconn  35461  ioosconn  35463  rellysconn  35467  fmlaomn0  35606  gonan0  35608  goaln0  35609  mpomulnzcnf  36515  fneref  36566  dnicn  36714  f1omptsnlem  37591  isbasisrelowl  37613  poimirlem27  37898  mblfinlem1  37908  mblfinlem2  37909  exidu1  38107  rngoideu  38154  isomliN  39615  idlaut  40472  resubf  42751  sn-subf  42799  mzpclall  43084  frmx  43270  frmy  43271  kelac2lem  43421  onsucf1o  43629  ontric3g  43878  clsk1indlem3  44399  wfaxpr  45354  icof  45577  natglobalincr  47235  sprsymrelf1  47856  fmtnof1  47895  prmdvdsfmtnof1  47947  usgrexmpl2trifr  48397  uspgrsprf1  48507  plusfreseq  48524  nnsgrpmgm  48536  nnsgrp  48537  nn0mnd  48539  2zrngamgm  48605  2zrngmmgm  48612  2zrngnmrid  48616  ldepslinc  48869  rrx2xpref1o  49078  rrx2plordisom  49083  rescofuf  49452  oppff1  49507