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

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.
StepHypRef Expression
1 eleq1 2718 . . . . . 6 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
21dvelimv 2369 . . . . 5 (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥𝐴 → ∀𝑦 𝑥𝐴))
3 rgen2a.1 . . . . . . 7 ((𝑥𝐴𝑦𝐴) → 𝜑)
43ex 449 . . . . . 6 (𝑥𝐴 → (𝑦𝐴𝜑))
54alimi 1779 . . . . 5 (∀𝑦 𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
62, 5syl6com 37 . . . 4 (𝑥𝐴 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦𝐴𝜑)))
7 eleq1 2718 . . . . . . 7 (𝑦 = 𝑥 → (𝑦𝐴𝑥𝐴))
87biimpd 219 . . . . . 6 (𝑦 = 𝑥 → (𝑦𝐴𝑥𝐴))
98, 4syli 39 . . . . 5 (𝑦 = 𝑥 → (𝑦𝐴𝜑))
109alimi 1779 . . . 4 (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦𝐴𝜑))
116, 10pm2.61d2 172 . . 3 (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
12 df-ral 2946 . . 3 (∀𝑦𝐴 𝜑 ↔ ∀𝑦(𝑦𝐴𝜑))
1311, 12sylibr 224 . 2 (𝑥𝐴 → ∀𝑦𝐴 𝜑)
1413rgen 2951 1 𝑥𝐴𝑦𝐴 𝜑
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator