Theorem rgen2 3169

Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3334 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 3121	. 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  3174  invdisjrab  5079  sosn  5706  isoid  7266  f1owe  7290  epweon  7711  epweonALT  7712  f1stres  7948  f2ndres  7949  fnwelem  8064  soseq  8092  issmo  8271  oawordeulem  8472  naddf  8599  ecopover  8748  unfilem2  9195  dffi2  9313  inficl  9315  fipwuni  9316  fisn  9317  dffi3  9321  cantnfvalf  9561  r111  9671  alephf1  9979  alephiso  9992  dfac5lem4  10020  dfac5lem4OLD  10022  kmlem9  10053  ackbij1lem17  10129  fin1a2lem2  10295  fin1a2lem4  10297  axcc2lem  10330  smobeth  10480  nqereu  10823  addpqf  10838  mulpqf  10840  genpdm  10896  axaddf  11039  axmulf  11040  subf  11365  mulnzcnf  11766  negiso  12105  cnref1o  12886  xaddf  13126  xmulf  13174  ioof  13350  om2uzf1oi  13860  om2uzisoi  13861  wrd2ind  14629  wwlktovf1  14864  reeff1  16029  divalglem9  16312  bitsf1  16357  smupf  16389  gcdf  16423  eucalgf  16494  qredeu  16569  1arith  16839  vdwapf  16884  xpsff1o  17471  catideu  17581  sscres  17730  fpwipodrs  18446  letsr  18499  mgmidmo  18534  frmdplusg  18728  efmndmgm  18759  smndex1mgm  18781  pwmnd  18811  mulgfval  18948  nmznsg  19047  efgmf  19592  efglem  19595  efgred  19627  isabli  19675  brric  20389  xrsmgm  21313  xrsds  21316  cnsubmlem  21321  cnsubrglem  21323  cnsubrglemOLD  21324  nn0srg  21344  rge0srg  21345  xrs1cmn  21349  xrge0subm  21350  xrge0omnd  21352  pzriprnglem5  21392  pzriprnglem8  21395  rzgrp  21530  fibas  22862  fctop  22889  cctop  22891  iccordt  23099  txuni2  23450  fsubbas  23752  zfbas  23781  ismeti  24211  dscmet  24458  qtopbaslem  24644  tgqioo  24686  xrsxmet  24696  xrsdsre  24697  retopconn  24716  iccconn  24717  divcnOLD  24755  divcn  24757  abscncf  24792  recncf  24793  imcncf  24794  cjcncf  24795  iimulcn  24832  iimulcnOLD  24833  icopnfhmeo  24839  iccpnfhmeo  24841  xrhmeo  24842  cnllycmp  24853  bndth  24855  iundisj2  25448  dyadf  25490  reefiso  26356  recosf1o  26442  cxpcn3  26656  sgmf  27053  2lgslem1b  27301  lrcut  27818  addsf  27894  negscut  27950  negsf1o  27965  subsf  27973  mulscutlem  28039  onsiso  28174  bdayn0sf1o  28264  zsoring  28301  tgjustf  28418  ercgrg  28462  2wspmdisj  30281  isabloi  30495  smcnlem  30641  cncph  30763  hvsubf  30959  hhip  31121  hhph  31122  helch  31187  hsn0elch  31192  hhssabloilem  31205  hhshsslem2  31212  shscli  31261  shintcli  31273  pjmf1  31660  idunop  31922  0cnop  31923  0cnfn  31924  idcnop  31925  idhmop  31926  0hmop  31927  adj0  31938  lnophsi  31945  lnopunii  31956  lnophmi  31962  nlelshi  32004  riesz4i  32007  cnlnadjlem6  32016  cnlnadjlem9  32019  adjcoi  32044  bra11  32052  pjhmopi  32090  iundisj2f  32534  iundisj2fi  32740  xrstos  32964  reofld  33281  xrge0slmod  33285  zringfrac  33491  iistmd  33869  cnre2csqima  33878  mndpluscn  33893  raddcn  33896  xrge0iifiso  33902  xrge0iifmhm  33906  xrge0pluscn  33907  cnzh  33935  rezh  33936  br2base  34237  sxbrsiga  34258  signswmnd  34525  cardpred  35057  nummin  35058  indispconn  35207  cnllysconn  35218  ioosconn  35220  rellysconn  35224  fmlaomn0  35363  gonan0  35365  goaln0  35366  mpomulnzcnf  36273  fneref  36324  dnicn  36466  f1omptsnlem  37310  isbasisrelowl  37332  poimirlem27  37627  mblfinlem1  37637  mblfinlem2  37638  exidu1  37836  rngoideu  37883  isomliN  39218  idlaut  40075  resubf  42354  sn-subf  42402  mzpclall  42700  frmx  42886  frmy  42887  kelac2lem  43037  onsucf1o  43245  ontric3g  43495  clsk1indlem3  44016  wfaxpr  44972  icof  45197  natglobalincr  46858  sprsymrelf1  47480  fmtnof1  47519  prmdvdsfmtnof1  47571  usgrexmpl2trifr  48021  uspgrsprf1  48131  plusfreseq  48148  nnsgrpmgm  48160  nnsgrp  48161  nn0mnd  48163  2zrngamgm  48229  2zrngmmgm  48236  2zrngnmrid  48240  ldepslinc  48494  rrx2xpref1o  48703  rrx2plordisom  48708  rescofuf  49078  oppff1  49133