Theorem rgen2 3177

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  rgen3  3182  invdisjrab  5094  sosn  5725  isoid  7304  f1owe  7328  epweon  7751  epweonALT  7752  f1stres  7992  f2ndres  7993  fnwelem  8110  soseq  8138  issmo  8317  oawordeulem  8518  naddf  8645  ecopover  8794  unfilem2  9255  dffi2  9374  inficl  9376  fipwuni  9377  fisn  9378  dffi3  9382  cantnfvalf  9618  r111  9728  alephf1  10038  alephiso  10051  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem9  10112  ackbij1lem17  10188  fin1a2lem2  10354  fin1a2lem4  10356  axcc2lem  10389  smobeth  10539  nqereu  10882  addpqf  10897  mulpqf  10899  genpdm  10955  axaddf  11098  axmulf  11099  subf  11423  mulnzcnf  11824  negiso  12163  cnref1o  12944  xaddf  13184  xmulf  13232  ioof  13408  om2uzf1oi  13918  om2uzisoi  13919  wrd2ind  14688  wwlktovf1  14923  reeff1  16088  divalglem9  16371  bitsf1  16416  smupf  16448  gcdf  16482  eucalgf  16553  qredeu  16628  1arith  16898  vdwapf  16943  xpsff1o  17530  catideu  17636  sscres  17785  fpwipodrs  18499  letsr  18552  mgmidmo  18587  frmdplusg  18781  efmndmgm  18812  smndex1mgm  18834  pwmnd  18864  mulgfval  19001  nmznsg  19100  efgmf  19643  efglem  19646  efgred  19678  isabli  19726  brric  20413  xrsmgm  21318  xrs1cmn  21323  xrge0subm  21324  xrsds  21326  cnsubmlem  21331  cnsubrglem  21333  cnsubrglemOLD  21334  nn0srg  21354  rge0srg  21355  pzriprnglem5  21395  pzriprnglem8  21398  rzgrp  21532  fibas  22864  fctop  22891  cctop  22893  iccordt  23101  txuni2  23452  fsubbas  23754  zfbas  23783  ismeti  24213  dscmet  24460  qtopbaslem  24646  tgqioo  24688  xrsxmet  24698  xrsdsre  24699  retopconn  24718  iccconn  24719  divcnOLD  24757  divcn  24759  abscncf  24794  recncf  24795  imcncf  24796  cjcncf  24797  iimulcn  24834  iimulcnOLD  24835  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  cnllycmp  24855  bndth  24857  iundisj2  25450  dyadf  25492  reefiso  26358  recosf1o  26444  cxpcn3  26658  sgmf  27055  2lgslem1b  27303  lrcut  27815  addsf  27889  negscut  27945  negsf1o  27960  subsf  27968  mulscutlem  28034  onsiso  28169  bdayn0sf1o  28259  tgjustf  28400  ercgrg  28444  2wspmdisj  30266  isabloi  30480  smcnlem  30626  cncph  30748  hvsubf  30944  hhip  31106  hhph  31107  helch  31172  hsn0elch  31177  hhssabloilem  31190  hhshsslem2  31197  shscli  31246  shintcli  31258  pjmf1  31645  idunop  31907  0cnop  31908  0cnfn  31909  idcnop  31910  idhmop  31911  0hmop  31912  adj0  31923  lnophsi  31930  lnopunii  31941  lnophmi  31947  nlelshi  31989  riesz4i  31992  cnlnadjlem6  32001  cnlnadjlem9  32004  adjcoi  32029  bra11  32037  pjhmopi  32075  iundisj2f  32519  iundisj2fi  32720  xrstos  32948  xrge0omnd  33025  reofld  33315  xrge0slmod  33319  zringfrac  33525  iistmd  33892  cnre2csqima  33901  mndpluscn  33916  raddcn  33919  xrge0iifiso  33925  xrge0iifmhm  33929  xrge0pluscn  33930  cnzh  33958  rezh  33959  br2base  34260  sxbrsiga  34281  signswmnd  34548  cardpred  35080  nummin  35081  indispconn  35221  cnllysconn  35232  ioosconn  35234  rellysconn  35238  fmlaomn0  35377  gonan0  35379  goaln0  35380  mpomulnzcnf  36287  fneref  36338  dnicn  36480  f1omptsnlem  37324  isbasisrelowl  37346  poimirlem27  37641  mblfinlem1  37651  mblfinlem2  37652  exidu1  37850  rngoideu  37897  isomliN  39232  idlaut  40090  resubf  42369  sn-subf  42417  mzpclall  42715  frmx  42902  frmy  42903  kelac2lem  43053  onsucf1o  43261  ontric3g  43511  clsk1indlem3  44032  wfaxpr  44988  icof  45213  natglobalincr  46875  sprsymrelf1  47497  fmtnof1  47536  prmdvdsfmtnof1  47588  usgrexmpl2trifr  48028  uspgrsprf1  48135  plusfreseq  48152  nnsgrpmgm  48164  nnsgrp  48165  nn0mnd  48167  2zrngamgm  48233  2zrngmmgm  48240  2zrngnmrid  48244  ldepslinc  48498  rrx2xpref1o  48707  rrx2plordisom  48712  rescofuf  49082  oppff1  49137