Theorem rgen2 3201

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2108  ∀wral 3136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3141

This theorem is referenced by:  rgen3  3202  invdisjrabw  5042  invdisjrab  5043  sosn  5631  isoid  7074  f1owe  7098  epweon  7489  f1stres  7705  f2ndres  7706  fnwelem  7817  issmo  7977  oawordeulem  8172  ecopover  8393  unfilem2  8775  dffi2  8879  inficl  8881  fipwuni  8882  fisn  8883  dffi3  8887  cantnfvalf  9120  r111  9196  alephf1  9503  alephiso  9516  dfac5lem4  9544  kmlem9  9576  ackbij1lem17  9650  fin1a2lem2  9815  fin1a2lem4  9817  axcc2lem  9850  smobeth  10000  nqereu  10343  addpqf  10358  mulpqf  10360  genpdm  10416  axaddf  10559  axmulf  10560  subf  10880  mulnzcnopr  11278  negiso  11613  cnref1o  12376  xaddf  12609  xmulf  12657  ioof  12827  om2uzf1oi  13313  om2uzisoi  13314  wrd2ind  14077  wwlktovf1  14313  reeff1  15465  divalglem9  15744  bitsf1  15787  smupf  15819  gcdf  15853  eucalgf  15919  qredeu  15994  1arith  16255  vdwapf  16300  xpsff1o  16832  catideu  16938  sscres  17085  fpwipodrs  17766  letsr  17829  mgmidmo  17862  frmdplusg  18011  efmndmgm  18042  smndex1mgm  18064  pwmnd  18094  mulgfval  18218  nmznsg  18312  efgmf  18831  efglem  18834  efgred  18866  isabli  18913  brric  19491  xrsmgm  20572  xrs1cmn  20577  xrge0subm  20578  xrsds  20580  cnsubmlem  20585  cnsubrglem  20587  nn0srg  20607  rge0srg  20608  rzgrp  20759  fibas  21577  fctop  21604  cctop  21606  iccordt  21814  txuni2  22165  fsubbas  22467  zfbas  22496  ismeti  22927  dscmet  23174  qtopbaslem  23359  tgqioo  23400  xrsxmet  23409  xrsdsre  23410  retopconn  23429  iccconn  23430  divcn  23468  abscncf  23501  recncf  23502  imcncf  23503  cjcncf  23504  iimulcn  23534  icopnfhmeo  23539  iccpnfhmeo  23541  xrhmeo  23542  cnllycmp  23552  bndth  23554  iundisj2  24142  dyadf  24184  reefiso  25028  recosf1o  25111  cxpcn3  25321  sgmf  25714  2lgslem1b  25960  tgjustf  26251  ercgrg  26295  2wspmdisj  28108  isabloi  28320  smcnlem  28466  cncph  28588  hvsubf  28784  hhip  28946  hhph  28947  helch  29012  hsn0elch  29017  hhssabloilem  29030  hhshsslem2  29037  shscli  29086  shintcli  29098  pjmf1  29485  idunop  29747  0cnop  29748  0cnfn  29749  idcnop  29750  idhmop  29751  0hmop  29752  adj0  29763  lnophsi  29770  lnopunii  29781  lnophmi  29787  nlelshi  29829  riesz4i  29832  cnlnadjlem6  29841  cnlnadjlem9  29844  adjcoi  29869  bra11  29877  pjhmopi  29915  iundisj2f  30332  iundisj2fi  30512  xrstos  30659  xrge0omnd  30705  reofld  30906  xrge0slmod  30910  iistmd  31138  cnre2csqima  31147  mndpluscn  31162  raddcn  31165  xrge0iifiso  31171  xrge0iifmhm  31175  xrge0pluscn  31176  cnzh  31204  rezh  31205  br2base  31520  sxbrsiga  31541  signswmnd  31820  indispconn  32474  cnllysconn  32485  ioosconn  32487  rellysconn  32491  fmlaomn0  32630  gonan0  32632  goaln0  32633  soseq  33089  fneref  33691  dnicn  33824  f1omptsnlem  34609  isbasisrelowl  34631  poimirlem27  34911  mblfinlem1  34921  mblfinlem2  34922  exidu1  35126  rngoideu  35173  isomliN  36367  idlaut  37224  resubf  39201  mzpclall  39314  frmx  39500  frmy  39501  kelac2lem  39654  ontric3g  39878  clsk1indlem3  40383  icof  41471  sprsymrelf1  43648  fmtnof1  43687  prmdvdsfmtnof1  43739  uspgrsprf1  44012  plusfreseq  44029  nnsgrpmgm  44073  nnsgrp  44074  nn0mnd  44076  2zrngamgm  44200  2zrngmmgm  44207  2zrngnmrid  44211  ldepslinc  44554  rrx2xpref1o  44695  rrx2plordisom  44700