MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgen2a Structured version   Visualization version   GIF version

Theorem rgen2a 2959
Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2324. (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.
StepHypRef Expression
1 eleq1 2675 . . . . . 6 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
21dvelimv 2325 . . . . 5 (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥𝐴 → ∀𝑦 𝑥𝐴))
3 rgen2a.1 . . . . . . 7 ((𝑥𝐴𝑦𝐴) → 𝜑)
43ex 448 . . . . . 6 (𝑥𝐴 → (𝑦𝐴𝜑))
54alimi 1729 . . . . 5 (∀𝑦 𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
62, 5syl6com 36 . . . 4 (𝑥𝐴 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦𝐴𝜑)))
7 eleq1 2675 . . . . . . 7 (𝑦 = 𝑥 → (𝑦𝐴𝑥𝐴))
87biimpd 217 . . . . . 6 (𝑦 = 𝑥 → (𝑦𝐴𝑥𝐴))
98, 4syli 38 . . . . 5 (𝑦 = 𝑥 → (𝑦𝐴𝜑))
109alimi 1729 . . . 4 (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦𝐴𝜑))
116, 10pm2.61d2 170 . . 3 (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
12 df-ral 2900 . . 3 (∀𝑦𝐴 𝜑 ↔ ∀𝑦(𝑦𝐴𝜑))
1311, 12sylibr 222 . 2 (𝑥𝐴 → ∀𝑦𝐴 𝜑)
1413rgen 2905 1 𝑥𝐴𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  wal 1472  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-clel 2605  df-ral 2900
This theorem is referenced by:  sosn  5101  isoid  6457  f1owe  6481  ordon  6851  fnwelem  7156  issmo  7309  oawordeulem  7498  ecopover  7715  ecopoverOLD  7716  unfilem2  8087  dffi2  8189  inficl  8191  fipwuni  8192  fisn  8193  dffi3  8197  cantnfvalf  8422  r111  8498  alephf1  8768  alephiso  8781  dfac5lem4  8809  kmlem9  8840  ackbij1lem17  8918  fin1a2lem2  9083  fin1a2lem4  9085  axcc2lem  9118  nqereu  9607  addpqf  9622  mulpqf  9624  genpdm  9680  axaddf  9822  axmulf  9823  subf  10134  mulnzcnopr  10522  negiso  10850  cnref1o  11659  xaddf  11888  xmulf  11931  ioof  12098  om2uzf1oi  12569  om2uzisoi  12570  wwlktovf1  13494  reeff1  14635  divalglem9  14908  bitsf1  14952  gcdf  15018  eucalgf  15080  qredeu  15156  1arith  15415  vdwapf  15460  catideu  16105  sscres  16252  fpwipodrs  16933  letsr  16996  mgmidmo  17028  frmdplusg  17160  nmznsg  17407  efgred  17930  isabli  17976  brric  18513  xrsmgm  19546  xrs1cmn  19551  xrge0subm  19552  xrsds  19554  cnsubmlem  19559  cnsubrglem  19561  nn0srg  19581  rge0srg  19582  fibas  20534  fctop  20560  cctop  20562  iccordt  20770  fsubbas  21423  zfbas  21452  ismeti  21881  dscmet  22128  qtopbaslem  22304  tgqioo  22343  xrsxmet  22352  xrsdsre  22353  retopcon  22372  iccconn  22373  iimulcn  22476  icopnfhmeo  22481  iccpnfhmeo  22483  xrhmeo  22484  iundisj2  23041  reefiso  23923  recosf1o  24002  rzgrp  24021  ercgrg  25130  isabloi  26558  cncph  26864  hvsubf  27062  hhip  27224  hhph  27225  helch  27290  hsn0elch  27295  hhssabloilem  27308  hhshsslem2  27315  shscli  27366  shintcli  27378  pjmf1  27765  idunop  28027  idhmop  28031  0hmop  28032  adj0  28043  lnopunii  28061  lnophmi  28067  riesz4i  28112  cnlnadjlem9  28124  adjcoi  28149  bra11  28157  pjhmopi  28195  iundisj2f  28591  iundisj2fi  28749  xrstos  28816  xrge0omnd  28848  reofld  28977  xrge0slmod  28981  iistmd  29082  cnre2csqima  29091  mndpluscn  29106  raddcn  29109  xrge0iifiso  29115  xrge0iifmhm  29119  xrge0pluscn  29120  br2base  29464  sxbrsiga  29485  signswmnd  29766  indispcon  30276  iooscon  30289  soseq  30801  f1omptsnlem  32155  isbasisrelowl  32178  poimirlem27  32402  exidu1  32621  rngoideu  32668  isomliN  33340  idlaut  34196  mzpclall  36104  kelac2lem  36448  clsk1indlem3  37157  icof  38202  prmdvdsfmtnof1  39835  plusfreseq  41557  nnsgrpmgm  41601  nnsgrp  41602  2zrngamgm  41724  2zrngmmgm  41731
  Copyright terms: Public domain W3C validator