Theorem rgen2 3197

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

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

This theorem is referenced by:  rgen3  3202  invdisjrab  5135  sosn  5775  isoid  7349  f1owe  7373  epweon  7794  epweonALT  7795  f1stres  8037  f2ndres  8038  fnwelem  8155  soseq  8183  issmo  8387  oawordeulem  8591  naddf  8718  ecopover  8860  unfilem2  9342  dffi2  9461  inficl  9463  fipwuni  9464  fisn  9465  dffi3  9469  cantnfvalf  9703  r111  9813  alephf1  10123  alephiso  10136  dfac5lem4  10164  dfac5lem4OLD  10166  kmlem9  10197  ackbij1lem17  10273  fin1a2lem2  10439  fin1a2lem4  10441  axcc2lem  10474  smobeth  10624  nqereu  10967  addpqf  10982  mulpqf  10984  genpdm  11040  axaddf  11183  axmulf  11184  subf  11508  mulnzcnf  11907  negiso  12246  cnref1o  13025  xaddf  13263  xmulf  13311  ioof  13484  om2uzf1oi  13991  om2uzisoi  13992  wrd2ind  14758  wwlktovf1  14993  reeff1  16153  divalglem9  16435  bitsf1  16480  smupf  16512  gcdf  16546  eucalgf  16617  qredeu  16692  1arith  16961  vdwapf  17006  xpsff1o  17614  catideu  17720  sscres  17871  fpwipodrs  18598  letsr  18651  mgmidmo  18686  frmdplusg  18880  efmndmgm  18911  smndex1mgm  18933  pwmnd  18963  mulgfval  19100  nmznsg  19199  efgmf  19746  efglem  19749  efgred  19781  isabli  19829  brric  20521  xrsmgm  21437  xrs1cmn  21442  xrge0subm  21443  xrsds  21445  cnsubmlem  21450  cnsubrglem  21452  cnsubrglemOLD  21453  nn0srg  21473  rge0srg  21474  pzriprnglem5  21514  pzriprnglem8  21517  rzgrp  21659  fibas  23000  fctop  23027  cctop  23029  iccordt  23238  txuni2  23589  fsubbas  23891  zfbas  23920  ismeti  24351  dscmet  24601  qtopbaslem  24795  tgqioo  24836  xrsxmet  24845  xrsdsre  24846  retopconn  24865  iccconn  24866  divcnOLD  24904  divcn  24906  abscncf  24941  recncf  24942  imcncf  24943  cjcncf  24944  iimulcn  24981  iimulcnOLD  24982  icopnfhmeo  24988  iccpnfhmeo  24990  xrhmeo  24991  cnllycmp  25002  bndth  25004  iundisj2  25598  dyadf  25640  reefiso  26507  recosf1o  26592  cxpcn3  26806  sgmf  27203  2lgslem1b  27451  lrcut  27956  addsf  28030  negscut  28086  negsf1o  28101  subsf  28109  mulscutlem  28172  tgjustf  28496  ercgrg  28540  2wspmdisj  30366  isabloi  30580  smcnlem  30726  cncph  30848  hvsubf  31044  hhip  31206  hhph  31207  helch  31272  hsn0elch  31277  hhssabloilem  31290  hhshsslem2  31297  shscli  31346  shintcli  31358  pjmf1  31745  idunop  32007  0cnop  32008  0cnfn  32009  idcnop  32010  idhmop  32011  0hmop  32012  adj0  32023  lnophsi  32030  lnopunii  32041  lnophmi  32047  nlelshi  32089  riesz4i  32092  cnlnadjlem6  32101  cnlnadjlem9  32104  adjcoi  32129  bra11  32137  pjhmopi  32175  iundisj2f  32610  iundisj2fi  32805  xrstos  32995  xrge0omnd  33071  reofld  33352  xrge0slmod  33356  zringfrac  33562  iistmd  33863  cnre2csqima  33872  mndpluscn  33887  raddcn  33890  xrge0iifiso  33896  xrge0iifmhm  33900  xrge0pluscn  33901  cnzh  33931  rezh  33932  br2base  34251  sxbrsiga  34272  signswmnd  34551  cardpred  35083  nummin  35084  indispconn  35219  cnllysconn  35230  ioosconn  35232  rellysconn  35236  fmlaomn0  35375  gonan0  35377  goaln0  35378  mpomulnzcnf  36282  fneref  36333  dnicn  36475  f1omptsnlem  37319  isbasisrelowl  37341  poimirlem27  37634  mblfinlem1  37644  mblfinlem2  37645  exidu1  37843  rngoideu  37890  isomliN  39221  idlaut  40079  resubf  42388  sn-subf  42435  mzpclall  42715  frmx  42902  frmy  42903  kelac2lem  43053  onsucf1o  43262  ontric3g  43512  clsk1indlem3  44033  wfaxpr  44952  icof  45162  natglobalincr  46831  sprsymrelf1  47421  fmtnof1  47460  prmdvdsfmtnof1  47512  usgrexmpl2trifr  47932  uspgrsprf1  47991  plusfreseq  48008  nnsgrpmgm  48020  nnsgrp  48021  nn0mnd  48023  2zrngamgm  48089  2zrngmmgm  48096  2zrngnmrid  48100  ldepslinc  48355  rrx2xpref1o  48568  rrx2plordisom  48573