Theorem rgen2 3203

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3078

This theorem is used by:  rgen3  3208  invdisjrab  5090  sosn  5738  isoid  7335  f1owe  7359  f1oweOLD  7360  epweon  7787  epweonALT  7788  f1stres  8023  f2ndres  8024  fnwelem  8141  soseq  8169  issmo  8349  oawordeulem  8555  naddf  8684  ecopover  8835  unfilem2  9291  dffi2  9408  inficl  9410  fipwuni  9411  fisn  9412  dffi3  9416  cantnfvalf  9659  r111  9775  alephf1  10157  alephiso  10170  dfac5lem4  10198  kmlem9  10230  ackbij1lem17  10306  fin1a2lem2  10472  fin1a2lem4  10474  axcc2lem  10507  smobeth  10664  nqereu  11007  addpqf  11022  mulpqf  11024  genpdm  11080  axaddf  11223  axmulf  11224  subf  11552  mulnzcnf  11955  negiso  12290  cnref1o  13106  xaddf  13347  xmulf  13395  ioof  13571  om2uzf1oi  14089  om2uzisoi  14090  wrd2ind  14865  wwlktovf1  15103  reeff1  16281  divalglem9  16564  bitsf1  16609  smupf  16641  gcdf  16677  eucalgf  16751  qredeu  16826  1arith  17098  vdwapf  17143  xpsff1o  17732  catideu  17842  sscres  17991  fpwipodrs  18707  letsr  18760  chninf  18802  mgmidmo  18831  frmdplusg  19043  efmndmgm  19074  smndex1mgm  19099  pwmnd  19136  mulgfval  19272  nmznsg  19371  efgmf  19920  efglem  19923  efgred  19955  isabli  20003  brric  20738  xrsmgm  21706  xrsds  21709  cnsubmlem  21714  cnsubrglem  21716  nn0srg  21736  rge0srg  21737  xrs1cmn  21741  xrge0subm  21742  xrge0omnd  21744  pzriprnglem5  21784  pzriprnglem8  21787  rzgrp  21922  fibas  23288  fctop  23315  cctop  23317  iccordt  23525  txuni2  23877  fsubbas  24179  zfbas  24208  ismeti  24637  dscmet  24884  qtopbaslem  25070  tgqioo  25112  xrsxmet  25122  xrsdsre  25123  retopconn  25142  iccconn  25143  divcn  25182  abscncf  25215  recncf  25216  imcncf  25217  cjcncf  25218  iimulcn  25252  icopnfhmeo  25257  iccpnfhmeo  25259  xrhmeo  25260  cnllycmp  25270  bndth  25272  iundisj2  25863  dyadf  25905  reefiso  26768  recosf1o  26856  cxpcn3  27069  sgmf  27465  2lgslem1b  27712  lrcut  28283  addsf  28361  negcut  28418  negsf1o  28433  subsf  28443  mulcutlem  28510  oniso  28650  bdayn0sf1o  28749  zsoring  28788  tgjustf  28928  ercgrg  28973  2wspmdisj  30931  isabloi  31146  smcnlem  31292  cncph  31414  hvsubf  31610  hhip  31772  hhph  31773  helch  31838  hsn0elch  31843  hhssabloilem  31856  hhshsslem2  31863  shscli  31912  shintcli  31924  pjmf1  32311  idunop  32573  0cnop  32574  0cnfn  32575  idcnop  32576  idhmop  32577  0hmop  32578  adj0  32589  lnophsi  32596  lnopunii  32607  lnophmi  32613  nlelshi  32655  riesz4i  32658  cnlnadjlem6  32667  cnlnadjlem9  32670  adjcoi  32695  bra11  32703  pjhmopi  32741  iundisj2f  33177  iundisj2fi  33382  xrstos  33564  reofld  33897  xrge0slmod  33902  zringfrac  34079  iistmd  34527  cnre2csqima  34536  mndpluscn  34551  raddcn  34554  xrge0iifiso  34560  xrge0iifmhm  34564  xrge0pluscn  34565  cnzh  34593  rezh  34594  br2base  34894  sxbrsiga  34915  signswmnd  35179  cardpred  35710  nummin  35711  indispconn  35978  cnllysconn  35989  ioosconn  35991  rellysconn  35995  fmlaomn0  36134  gonan0  36136  goaln0  36137  mpomulnzcnf  37068  fneref  37118  dnicn  37338  f1omptsnlem  38239  isbasisrelowl  38261  poimirlem27  38545  mblfinlem1  38555  mblfinlem2  38556  exidu1  38770  rngoideu  38817  isomliN  40276  idlaut  41133  resubf  43412  sn-subf  43460  mzpclall  43717  frmx  43899  frmy  43900  kelac2lem  44050  onsucf1o  44258  ontric3g  44507  clsk1indlem3  45028  wfaxpr  45966  hashomiso  45993  icof  46201  sprsymrelf1  48547  fmtnof1  48589  prmdvdsfmtnof1  48641  usgrexmpl2trifr  49104  uspgrsprf1  49214  plusfreseq  49230  nnsgrpmgm  49242  nnsgrp  49243  nn0mnd  49245  2zrngamgm  49311  2zrngmmgm  49318  2zrngnmrid  49322  ldepslinc  49590  rrx2xpref1o  49799  rrx2plordisom  49804  rescofuf  50170  oppff1  50225