Theorem rgen2a 3006

Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2368. (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 2718	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
2	1	dvelimv 2369	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴))
3		rgen2a.1	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)
4	3	ex 449	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝜑))
5	4	alimi 1779	. . . . 5 ⊢ (∀𝑦 𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
6	2, 5	syl6com 37	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)))
7		eleq1 2718	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	biimpd 219	. . . . . 6 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴))
9	8, 4	syli 39	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑))
10	9	alimi 1779	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
11	6, 10	pm2.61d2 172	. . 3 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
12		df-ral 2946	. . 3 ⊢ (∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
13	11, 12	sylibr 224	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜑)
14	13	rgen 2951	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1521   ∈ wcel 2030  ∀wral 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-ral 2946

This theorem is referenced by:  sosn  5222  isoid  6619  f1owe  6643  ordon  7024  fnwelem  7337  issmo  7490  oawordeulem  7679  ecopover  7894  unfilem2  8266  dffi2  8370  inficl  8372  fipwuni  8373  fisn  8374  dffi3  8378  cantnfvalf  8600  r111  8676  alephf1  8946  alephiso  8959  dfac5lem4  8987  kmlem9  9018  ackbij1lem17  9096  fin1a2lem2  9261  fin1a2lem4  9263  axcc2lem  9296  nqereu  9789  addpqf  9804  mulpqf  9806  genpdm  9862  axaddf  10004  axmulf  10005  subf  10321  mulnzcnopr  10711  negiso  11041  cnref1o  11865  xaddf  12093  xmulf  12140  ioof  12309  om2uzf1oi  12792  om2uzisoi  12793  wwlktovf1  13746  reeff1  14894  divalglem9  15171  bitsf1  15215  gcdf  15281  eucalgf  15343  qredeu  15419  1arith  15678  vdwapf  15723  catideu  16383  sscres  16530  fpwipodrs  17211  letsr  17274  mgmidmo  17306  frmdplusg  17438  nmznsg  17685  efgred  18207  isabli  18253  brric  18792  xrsmgm  19829  xrs1cmn  19834  xrge0subm  19835  xrsds  19837  cnsubmlem  19842  cnsubrglem  19844  nn0srg  19864  rge0srg  19865  fibas  20829  fctop  20856  cctop  20858  iccordt  21066  fsubbas  21718  zfbas  21747  ismeti  22177  dscmet  22424  qtopbaslem  22609  tgqioo  22650  xrsxmet  22659  xrsdsre  22660  retopconn  22679  iccconn  22680  iimulcn  22784  icopnfhmeo  22789  iccpnfhmeo  22791  xrhmeo  22792  iundisj2  23363  reefiso  24247  recosf1o  24326  rzgrp  24345  ercgrg  25457  2wspmdisj  27317  isabloi  27533  cncph  27802  hvsubf  28000  hhip  28162  hhph  28163  helch  28228  hsn0elch  28233  hhssabloilem  28246  hhshsslem2  28253  shscli  28304  shintcli  28316  pjmf1  28703  idunop  28965  idhmop  28969  0hmop  28970  adj0  28981  lnopunii  28999  lnophmi  29005  riesz4i  29050  cnlnadjlem9  29062  adjcoi  29087  bra11  29095  pjhmopi  29133  iundisj2f  29529  iundisj2fi  29684  xrstos  29807  xrge0omnd  29839  reofld  29968  xrge0slmod  29972  iistmd  30076  cnre2csqima  30085  mndpluscn  30100  raddcn  30103  xrge0iifiso  30109  xrge0iifmhm  30113  xrge0pluscn  30114  br2base  30459  sxbrsiga  30480  signswmnd  30762  indispconn  31342  ioosconn  31355  soseq  31879  f1omptsnlem  33313  isbasisrelowl  33336  poimirlem27  33566  exidu1  33785  rngoideu  33832  isomliN  34844  idlaut  35700  mzpclall  37607  kelac2lem  37951  clsk1indlem3  38658  icof  39725  prmdvdsfmtnof1  41824  sprsymrelf1  42071  uspgrsprf1  42080  plusfreseq  42097  nnsgrpmgm  42141  nnsgrp  42142  2zrngamgm  42264  2zrngmmgm  42271