Theorem rgen2a 2977

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384  ∀wal 1481   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-ral 2917

This theorem is referenced by:  sosn  5188  isoid  6579  f1owe  6603  ordon  6982  fnwelem  7292  issmo  7445  oawordeulem  7634  ecopover  7851  ecopoverOLD  7852  unfilem2  8225  dffi2  8329  inficl  8331  fipwuni  8332  fisn  8333  dffi3  8337  cantnfvalf  8562  r111  8638  alephf1  8908  alephiso  8921  dfac5lem4  8949  kmlem9  8980  ackbij1lem17  9058  fin1a2lem2  9223  fin1a2lem4  9225  axcc2lem  9258  nqereu  9751  addpqf  9766  mulpqf  9768  genpdm  9824  axaddf  9966  axmulf  9967  subf  10283  mulnzcnopr  10673  negiso  11003  cnref1o  11827  xaddf  12055  xmulf  12102  ioof  12271  om2uzf1oi  12752  om2uzisoi  12753  wwlktovf1  13700  reeff1  14850  divalglem9  15124  bitsf1  15168  gcdf  15234  eucalgf  15296  qredeu  15372  1arith  15631  vdwapf  15676  catideu  16336  sscres  16483  fpwipodrs  17164  letsr  17227  mgmidmo  17259  frmdplusg  17391  nmznsg  17638  efgred  18161  isabli  18207  brric  18744  xrsmgm  19781  xrs1cmn  19786  xrge0subm  19787  xrsds  19789  cnsubmlem  19794  cnsubrglem  19796  nn0srg  19816  rge0srg  19817  fibas  20781  fctop  20808  cctop  20810  iccordt  21018  fsubbas  21671  zfbas  21700  ismeti  22130  dscmet  22377  qtopbaslem  22562  tgqioo  22603  xrsxmet  22612  xrsdsre  22613  retopconn  22632  iccconn  22633  iimulcn  22737  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  iundisj2  23317  reefiso  24202  recosf1o  24281  rzgrp  24300  ercgrg  25412  2wspmdisj  27201  isabloi  27405  cncph  27674  hvsubf  27872  hhip  28034  hhph  28035  helch  28100  hsn0elch  28105  hhssabloilem  28118  hhshsslem2  28125  shscli  28176  shintcli  28188  pjmf1  28575  idunop  28837  idhmop  28841  0hmop  28842  adj0  28853  lnopunii  28871  lnophmi  28877  riesz4i  28922  cnlnadjlem9  28934  adjcoi  28959  bra11  28967  pjhmopi  29005  iundisj2f  29403  iundisj2fi  29556  xrstos  29679  xrge0omnd  29711  reofld  29840  xrge0slmod  29844  iistmd  29948  cnre2csqima  29957  mndpluscn  29972  raddcn  29975  xrge0iifiso  29981  xrge0iifmhm  29985  xrge0pluscn  29986  br2base  30331  sxbrsiga  30352  signswmnd  30634  indispconn  31216  ioosconn  31229  soseq  31751  f1omptsnlem  33183  isbasisrelowl  33206  poimirlem27  33436  exidu1  33655  rngoideu  33702  isomliN  34526  idlaut  35382  mzpclall  37290  kelac2lem  37634  clsk1indlem3  38341  icof  39411  prmdvdsfmtnof1  41499  sprsymrelf1  41746  uspgrsprf1  41755  plusfreseq  41772  nnsgrpmgm  41816  nnsgrp  41817  2zrngamgm  41939  2zrngmmgm  41946