Theorem rgen2a 3176

Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2387. (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 2853	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
2	1	dvelimv 2388	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴))
3		rgen2a.1	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)
4	3	ex 405	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝜑))
5	4	alimi 1774	. . . . 5 ⊢ (∀𝑦 𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
6	2, 5	syl6com 37	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)))
7		eleq1 2853	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	biimpd 221	. . . . . 6 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴))
9	8, 4	syli 39	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑))
10	9	alimi 1774	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
11	6, 10	pm2.61d2 174	. . 3 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
12		df-ral 3093	. . 3 ⊢ (∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
13	11, 12	sylibr 226	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜑)
14	13	rgen 3098	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 387  ∀wal 1505   ∈ wcel 2050  ∀wral 3088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-cleq 2771  df-clel 2846  df-ral 3093

This theorem is referenced by:  isoid  6907  f1owe  6931  epweon  7315  fnwelem  7632  oawordeulem  7983  ecopover  8203  unfilem2  8580  dffi2  8684  inficl  8686  fipwuni  8687  fisn  8688  dffi3  8692  cantnfvalf  8924  r111  9000  alephf1  9307  alephiso  9320  dfac5lem4  9348  kmlem9  9380  ackbij1lem17  9458  fin1a2lem2  9623  fin1a2lem4  9625  axcc2lem  9658  nqereu  10151  addpqf  10166  mulpqf  10168  genpdm  10224  axaddf  10367  axmulf  10368  subf  10690  mulnzcnopr  11089  negiso  11424  cnref1o  12202  xaddf  12437  xmulf  12484  ioof  12654  om2uzf1oi  13139  om2uzisoi  13140  wwlktovf1  14185  reeff1  15336  divalglem9  15615  bitsf1  15658  gcdf  15724  eucalgf  15786  qredeu  15861  1arith  16122  vdwapf  16167  catideu  16807  sscres  16954  fpwipodrs  17635  letsr  17698  mgmidmo  17730  frmdplusg  17863  nmznsg  18110  efgred  18637  isabli  18683  brric  19225  xrsmgm  20285  xrs1cmn  20290  xrge0subm  20291  xrsds  20293  cnsubmlem  20298  cnsubrglem  20300  nn0srg  20320  rge0srg  20321  rzgrp  20472  fibas  21292  fctop  21319  cctop  21321  iccordt  21529  fsubbas  22182  zfbas  22211  ismeti  22641  dscmet  22888  qtopbaslem  23073  tgqioo  23114  xrsxmet  23123  xrsdsre  23124  retopconn  23143  iccconn  23144  iimulcn  23248  icopnfhmeo  23253  iccpnfhmeo  23255  xrhmeo  23256  iundisj2  23856  reefiso  24742  recosf1o  24823  2lgslem1b  25673  tgjustf  25964  ercgrg  26008  2wspmdisj  27874  isabloi  28108  cncph  28376  hvsubf  28574  hhip  28736  hhph  28737  helch  28802  hsn0elch  28807  hhssabloilem  28820  hhshsslem2  28827  shscli  28878  shintcli  28890  pjmf1  29277  idunop  29539  idhmop  29543  0hmop  29544  adj0  29555  lnopunii  29573  lnophmi  29579  riesz4i  29624  cnlnadjlem9  29636  adjcoi  29661  bra11  29669  pjhmopi  29707  iundisj2f  30109  iundisj2fi  30272  xrstos  30398  xrge0omnd  30430  reofld  30592  xrge0slmod  30596  iistmd  30789  cnre2csqima  30798  mndpluscn  30813  raddcn  30816  xrge0iifiso  30822  xrge0iifmhm  30826  xrge0pluscn  30827  br2base  31172  sxbrsiga  31193  signswmnd  31473  indispconn  32066  ioosconn  32079  soseq  32617  f1omptsnlem  34059  isbasisrelowl  34081  poimirlem27  34360  exidu1  34576  rngoideu  34623  isomliN  35820  idlaut  36677  resubf  38644  mzpclall  38719  kelac2lem  39060  clsk1indlem3  39756  icof  40908  sprsymrelf1  43027  prmdvdsfmtnof1  43118  uspgrsprf1  43391  plusfreseq  43408  nnsgrpmgm  43452  nnsgrp  43453  2zrngamgm  43575  2zrngmmgm  43582  rrx2xpref1o  44074  rrx2plordisom  44079