Theorem rgen2a 2960

Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2325. (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2020.) (Proof modification is discouraged.)

Hypothesis

Ref	Expression
rgen2a.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)

Assertion

Ref	Expression
rgen2a	⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑

Distinct variable group:   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem rgen2a

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2676	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
2	1	dvelimv 2326	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴))
3		rgen2a.1	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)
4	3	ex 449	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝜑))
5	4	alimi 1730	. . . . 5 ⊢ (∀𝑦 𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
6	2, 5	syl6com 36	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)))
7		eleq1 2676	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	biimpd 218	. . . . . 6 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴))
9	8, 4	syli 38	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑))
10	9	alimi 1730	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
11	6, 10	pm2.61d2 171	. . 3 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
12		df-ral 2901	. . 3 ⊢ (∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
13	11, 12	sylibr 223	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜑)
14	13	rgen 2906	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1473   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-ral 2901

This theorem is referenced by:  sosn  5111  isoid  6479  f1owe  6503  ordon  6874  fnwelem  7179  issmo  7332  oawordeulem  7521  ecopover  7738  ecopoverOLD  7739  unfilem2  8110  dffi2  8212  inficl  8214  fipwuni  8215  fisn  8216  dffi3  8220  cantnfvalf  8445  r111  8521  alephf1  8791  alephiso  8804  dfac5lem4  8832  kmlem9  8863  ackbij1lem17  8941  fin1a2lem2  9106  fin1a2lem4  9108  axcc2lem  9141  nqereu  9630  addpqf  9645  mulpqf  9647  genpdm  9703  axaddf  9845  axmulf  9846  subf  10162  mulnzcnopr  10552  negiso  10880  cnref1o  11703  xaddf  11929  xmulf  11974  ioof  12142  om2uzf1oi  12614  om2uzisoi  12615  wwlktovf1  13548  reeff1  14689  divalglem9  14962  bitsf1  15006  gcdf  15072  eucalgf  15134  qredeu  15210  1arith  15469  vdwapf  15514  catideu  16159  sscres  16306  fpwipodrs  16987  letsr  17050  mgmidmo  17082  frmdplusg  17214  nmznsg  17461  efgred  17984  isabli  18030  brric  18567  xrsmgm  19600  xrs1cmn  19605  xrge0subm  19606  xrsds  19608  cnsubmlem  19613  cnsubrglem  19615  nn0srg  19635  rge0srg  19636  fibas  20592  fctop  20618  cctop  20620  iccordt  20828  fsubbas  21481  zfbas  21510  ismeti  21940  dscmet  22187  qtopbaslem  22372  tgqioo  22411  xrsxmet  22420  xrsdsre  22421  retopcon  22440  iccconn  22441  iimulcn  22545  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  iundisj2  23124  reefiso  24006  recosf1o  24085  rzgrp  24104  ercgrg  25212  isabloi  26789  cncph  27058  hvsubf  27256  hhip  27418  hhph  27419  helch  27484  hsn0elch  27489  hhssabloilem  27502  hhshsslem2  27509  shscli  27560  shintcli  27572  pjmf1  27959  idunop  28221  idhmop  28225  0hmop  28226  adj0  28237  lnopunii  28255  lnophmi  28261  riesz4i  28306  cnlnadjlem9  28318  adjcoi  28343  bra11  28351  pjhmopi  28389  iundisj2f  28785  iundisj2fi  28943  xrstos  29010  xrge0omnd  29042  reofld  29171  xrge0slmod  29175  iistmd  29276  cnre2csqima  29285  mndpluscn  29300  raddcn  29303  xrge0iifiso  29309  xrge0iifmhm  29313  xrge0pluscn  29314  br2base  29658  sxbrsiga  29679  signswmnd  29960  indispcon  30470  iooscon  30483  soseq  30995  f1omptsnlem  32359  isbasisrelowl  32382  poimirlem27  32606  exidu1  32825  rngoideu  32872  isomliN  33544  idlaut  34400  mzpclall  36308  kelac2lem  36652  clsk1indlem3  37361  icof  38406  prmdvdsfmtnof1  40037  plusfreseq  41562  nnsgrpmgm  41606  nnsgrp  41607  2zrngamgm  41729  2zrngmmgm  41736