Theorem rgen2 3195

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  ∀wral 3058

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3059

This theorem is referenced by:  rgen3  3200  invdisjrabw  5137  invdisjrab  5138  sosn  5768  isoid  7343  f1owe  7367  epweon  7783  epweonALT  7784  f1stres  8023  f2ndres  8024  fnwelem  8142  soseq  8170  issmo  8375  oawordeulem  8581  naddf  8708  ecopover  8846  unfilem2  9342  dffi2  9454  inficl  9456  fipwuni  9457  fisn  9458  dffi3  9462  cantnfvalf  9696  r111  9806  alephf1  10116  alephiso  10129  dfac5lem4  10157  kmlem9  10189  ackbij1lem17  10267  fin1a2lem2  10432  fin1a2lem4  10434  axcc2lem  10467  smobeth  10617  nqereu  10960  addpqf  10975  mulpqf  10977  genpdm  11033  axaddf  11176  axmulf  11177  subf  11500  mulnzcnf  11898  negiso  12232  cnref1o  13007  xaddf  13243  xmulf  13291  ioof  13464  om2uzf1oi  13958  om2uzisoi  13959  wrd2ind  14713  wwlktovf1  14948  reeff1  16104  divalglem9  16385  bitsf1  16428  smupf  16460  gcdf  16494  eucalgf  16561  qredeu  16636  1arith  16903  vdwapf  16948  xpsff1o  17556  catideu  17662  sscres  17813  fpwipodrs  18539  letsr  18592  mgmidmo  18627  frmdplusg  18813  efmndmgm  18844  smndex1mgm  18866  pwmnd  18896  mulgfval  19032  nmznsg  19130  efgmf  19675  efglem  19678  efgred  19710  isabli  19758  brric  20450  xrsmgm  21341  xrs1cmn  21346  xrge0subm  21347  xrsds  21349  cnsubmlem  21354  cnsubrglem  21356  cnsubrglemOLD  21357  nn0srg  21377  rge0srg  21378  pzriprnglem5  21418  pzriprnglem8  21421  rzgrp  21562  fibas  22900  fctop  22927  cctop  22929  iccordt  23138  txuni2  23489  fsubbas  23791  zfbas  23820  ismeti  24251  dscmet  24501  qtopbaslem  24695  tgqioo  24736  xrsxmet  24745  xrsdsre  24746  retopconn  24765  iccconn  24766  divcnOLD  24804  divcn  24806  abscncf  24841  recncf  24842  imcncf  24843  cjcncf  24844  iimulcn  24881  iimulcnOLD  24882  icopnfhmeo  24888  iccpnfhmeo  24890  xrhmeo  24891  cnllycmp  24902  bndth  24904  iundisj2  25498  dyadf  25540  reefiso  26405  recosf1o  26489  cxpcn3  26703  sgmf  27097  2lgslem1b  27345  lrcut  27849  addsf  27919  negscut  27971  negsf1o  27986  mulscutlem  28051  tgjustf  28297  ercgrg  28341  2wspmdisj  30167  isabloi  30381  smcnlem  30527  cncph  30649  hvsubf  30845  hhip  31007  hhph  31008  helch  31073  hsn0elch  31078  hhssabloilem  31091  hhshsslem2  31098  shscli  31147  shintcli  31159  pjmf1  31546  idunop  31808  0cnop  31809  0cnfn  31810  idcnop  31811  idhmop  31812  0hmop  31813  adj0  31824  lnophsi  31831  lnopunii  31842  lnophmi  31848  nlelshi  31890  riesz4i  31893  cnlnadjlem6  31902  cnlnadjlem9  31905  adjcoi  31930  bra11  31938  pjhmopi  31976  iundisj2f  32401  iundisj2fi  32586  xrstos  32758  xrge0omnd  32812  reofld  33080  xrge0slmod  33084  zringfrac  33277  iistmd  33536  cnre2csqima  33545  mndpluscn  33560  raddcn  33563  xrge0iifiso  33569  xrge0iifmhm  33573  xrge0pluscn  33574  cnzh  33604  rezh  33605  br2base  33922  sxbrsiga  33943  signswmnd  34222  cardpred  34746  nummin  34747  indispconn  34877  cnllysconn  34888  ioosconn  34890  rellysconn  34894  fmlaomn0  35033  gonan0  35035  goaln0  35036  mpomulnzcnf  35816  fneref  35867  dnicn  36000  f1omptsnlem  36848  isbasisrelowl  36870  poimirlem27  37153  mblfinlem1  37163  mblfinlem2  37164  exidu1  37362  rngoideu  37409  isomliN  38743  idlaut  39601  resubf  41967  sn-subf  42014  mzpclall  42178  frmx  42365  frmy  42366  kelac2lem  42519  onsucf1o  42732  ontric3g  42983  clsk1indlem3  43504  icof  44622  natglobalincr  46292  sprsymrelf1  46865  fmtnof1  46904  prmdvdsfmtnof1  46956  uspgrsprf1  47287  plusfreseq  47304  nnsgrpmgm  47316  nnsgrp  47317  nn0mnd  47319  2zrngamgm  47385  2zrngmmgm  47392  2zrngnmrid  47396  ldepslinc  47655  rrx2xpref1o  47869  rrx2plordisom  47874