Theorem rgen2 3129

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2110  ∀wral 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3071

This theorem is referenced by:  rgen3  3130  invdisjrabw  5064  invdisjrab  5065  sosn  5674  isoid  7196  f1owe  7220  epweon  7619  epweonOLD  7620  f1stres  7848  f2ndres  7849  fnwelem  7963  issmo  8170  oawordeulem  8370  ecopover  8593  unfilem2  9057  dffi2  9160  inficl  9162  fipwuni  9163  fisn  9164  dffi3  9168  cantnfvalf  9401  r111  9534  alephf1  9842  alephiso  9855  dfac5lem4  9883  kmlem9  9915  ackbij1lem17  9993  fin1a2lem2  10158  fin1a2lem4  10160  axcc2lem  10193  smobeth  10343  nqereu  10686  addpqf  10701  mulpqf  10703  genpdm  10759  axaddf  10902  axmulf  10903  subf  11223  mulnzcnopr  11621  negiso  11955  cnref1o  12724  xaddf  12957  xmulf  13005  ioof  13178  om2uzf1oi  13671  om2uzisoi  13672  wrd2ind  14434  wwlktovf1  14670  reeff1  15827  divalglem9  16108  bitsf1  16151  smupf  16183  gcdf  16217  eucalgf  16286  qredeu  16361  1arith  16626  vdwapf  16671  xpsff1o  17276  catideu  17382  sscres  17533  fpwipodrs  18256  letsr  18309  mgmidmo  18342  frmdplusg  18491  efmndmgm  18522  smndex1mgm  18544  pwmnd  18574  mulgfval  18700  nmznsg  18794  efgmf  19317  efglem  19320  efgred  19352  isabli  19399  brric  19986  xrsmgm  20631  xrs1cmn  20636  xrge0subm  20637  xrsds  20639  cnsubmlem  20644  cnsubrglem  20646  nn0srg  20666  rge0srg  20667  rzgrp  20826  fibas  22125  fctop  22152  cctop  22154  iccordt  22363  txuni2  22714  fsubbas  23016  zfbas  23045  ismeti  23476  dscmet  23726  qtopbaslem  23920  tgqioo  23961  xrsxmet  23970  xrsdsre  23971  retopconn  23990  iccconn  23991  divcn  24029  abscncf  24062  recncf  24063  imcncf  24064  cjcncf  24065  iimulcn  24099  icopnfhmeo  24104  iccpnfhmeo  24106  xrhmeo  24107  cnllycmp  24117  bndth  24119  iundisj2  24711  dyadf  24753  reefiso  25605  recosf1o  25689  cxpcn3  25899  sgmf  26292  2lgslem1b  26538  tgjustf  26832  ercgrg  26876  2wspmdisj  28697  isabloi  28909  smcnlem  29055  cncph  29177  hvsubf  29373  hhip  29535  hhph  29536  helch  29601  hsn0elch  29606  hhssabloilem  29619  hhshsslem2  29626  shscli  29675  shintcli  29687  pjmf1  30074  idunop  30336  0cnop  30337  0cnfn  30338  idcnop  30339  idhmop  30340  0hmop  30341  adj0  30352  lnophsi  30359  lnopunii  30370  lnophmi  30376  nlelshi  30418  riesz4i  30421  cnlnadjlem6  30430  cnlnadjlem9  30433  adjcoi  30458  bra11  30466  pjhmopi  30504  iundisj2f  30925  iundisj2fi  31114  xrstos  31284  xrge0omnd  31333  reofld  31540  xrge0slmod  31544  iistmd  31848  cnre2csqima  31857  mndpluscn  31872  raddcn  31875  xrge0iifiso  31881  xrge0iifmhm  31885  xrge0pluscn  31886  cnzh  31916  rezh  31917  br2base  32232  sxbrsiga  32253  signswmnd  32532  cardpred  33058  nummin  33059  indispconn  33192  cnllysconn  33203  ioosconn  33205  rellysconn  33209  fmlaomn0  33348  gonan0  33350  goaln0  33351  soseq  33799  lrcut  34079  fneref  34535  dnicn  34668  f1omptsnlem  35503  isbasisrelowl  35525  poimirlem27  35800  mblfinlem1  35810  mblfinlem2  35811  exidu1  36010  rngoideu  36057  isomliN  37249  idlaut  38106  resubf  40361  sn-subf  40407  mzpclall  40546  frmx  40732  frmy  40733  kelac2lem  40886  ontric3g  41108  clsk1indlem3  41623  icof  42729  sprsymrelf1  44917  fmtnof1  44956  prmdvdsfmtnof1  45008  uspgrsprf1  45278  plusfreseq  45295  nnsgrpmgm  45339  nnsgrp  45340  nn0mnd  45342  2zrngamgm  45466  2zrngmmgm  45473  2zrngnmrid  45477  ldepslinc  45819  rrx2xpref1o  46033  rrx2plordisom  46038