Theorem rgen2 3205

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080

This theorem is referenced by:  rgen3  3210  invdisjrab  5096  sosn  5748  isoid  7327  f1owe  7351  epweon  7770  epweonALT  7771  f1stres  8006  f2ndres  8007  fnwelem  8123  soseq  8151  issmo  8331  oawordeulem  8535  naddf  8664  ecopover  8815  unfilem2  9262  dffi2  9379  inficl  9381  fipwuni  9382  fisn  9383  dffi3  9387  cantnfvalf  9630  r111  9743  alephf1  10065  alephiso  10078  dfac5lem4  10106  kmlem9  10138  ackbij1lem17  10214  fin1a2lem2  10380  fin1a2lem4  10382  axcc2lem  10415  smobeth  10566  nqereu  10909  addpqf  10924  mulpqf  10926  genpdm  10982  axaddf  11125  axmulf  11126  subf  11454  mulnzcnf  11855  negiso  12190  cnref1o  13004  xaddf  13245  xmulf  13293  ioof  13469  om2uzf1oi  13985  om2uzisoi  13986  wrd2ind  14756  wwlktovf1  14990  reeff1  16171  divalglem9  16454  bitsf1  16499  smupf  16531  gcdf  16565  eucalgf  16636  qredeu  16711  1arith  16982  vdwapf  17027  xpsff1o  17616  catideu  17726  sscres  17875  fpwipodrs  18591  letsr  18644  chninf  18686  mgmidmo  18713  frmdplusg  18908  efmndmgm  18939  smndex1mgm  18964  pwmnd  18994  mulgfval  19130  nmznsg  19229  efgmf  19778  efglem  19781  efgred  19813  isabli  19861  brric  20593  xrsmgm  21557  xrsds  21560  cnsubmlem  21565  cnsubrglem  21567  nn0srg  21587  rge0srg  21588  xrs1cmn  21592  xrge0subm  21593  xrge0omnd  21595  pzriprnglem5  21635  pzriprnglem8  21638  rzgrp  21773  fibas  23134  fctop  23161  cctop  23163  iccordt  23371  txuni2  23722  fsubbas  24024  zfbas  24053  ismeti  24482  dscmet  24729  qtopbaslem  24915  tgqioo  24957  xrsxmet  24967  xrsdsre  24968  retopconn  24987  iccconn  24988  divcn  25027  abscncf  25060  recncf  25061  imcncf  25062  cjcncf  25063  iimulcn  25097  icopnfhmeo  25102  iccpnfhmeo  25104  xrhmeo  25105  cnllycmp  25115  bndth  25117  iundisj2  25708  dyadf  25750  reefiso  26611  recosf1o  26700  cxpcn3  26913  sgmf  27309  2lgslem1b  27556  lrcut  28097  addsf  28175  negcut  28232  negsf1o  28247  subsf  28257  mulcutlem  28324  oniso  28464  bdayn0sf1o  28563  zsoring  28602  tgjustf  28742  ercgrg  28786  2wspmdisj  30688  isabloi  30903  smcnlem  31049  cncph  31171  hvsubf  31367  hhip  31529  hhph  31530  helch  31595  hsn0elch  31600  hhssabloilem  31613  hhshsslem2  31620  shscli  31669  shintcli  31681  pjmf1  32068  idunop  32330  0cnop  32331  0cnfn  32332  idcnop  32333  idhmop  32334  0hmop  32335  adj0  32346  lnophsi  32353  lnopunii  32364  lnophmi  32370  nlelshi  32412  riesz4i  32415  cnlnadjlem6  32424  cnlnadjlem9  32427  adjcoi  32452  bra11  32460  pjhmopi  32498  iundisj2f  32935  iundisj2fi  33142  xrstos  33330  reofld  33663  xrge0slmod  33668  zringfrac  33844  iistmd  34292  cnre2csqima  34301  mndpluscn  34316  raddcn  34319  xrge0iifiso  34325  xrge0iifmhm  34329  xrge0pluscn  34330  cnzh  34358  rezh  34359  br2base  34659  sxbrsiga  34680  signswmnd  34944  cardpred  35483  nummin  35484  indispconn  35726  cnllysconn  35737  ioosconn  35739  rellysconn  35743  fmlaomn0  35882  gonan0  35884  goaln0  35885  mpomulnzcnf  36811  fneref  36861  dnicn  37081  f1omptsnlem  37982  isbasisrelowl  38004  poimirlem27  38298  mblfinlem1  38308  mblfinlem2  38309  exidu1  38507  rngoideu  38554  isomliN  40013  idlaut  40870  resubf  43142  sn-subf  43190  mzpclall  43458  frmx  43640  frmy  43641  kelac2lem  43791  onsucf1o  43999  ontric3g  44248  clsk1indlem3  44769  wfaxpr  45707  hashomiso  45734  icof  45935  natglobalincr  47593  sprsymrelf1  48245  fmtnof1  48287  prmdvdsfmtnof1  48339  usgrexmpl2trifr  48802  uspgrsprf1  48912  plusfreseq  48929  nnsgrpmgm  48941  nnsgrp  48942  nn0mnd  48944  2zrngamgm  49010  2zrngmmgm  49017  2zrngnmrid  49021  ldepslinc  49289  rrx2xpref1o  49498  rrx2plordisom  49503  rescofuf  49871  oppff1  49926