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

Theorem rgen2a 3172
Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2501. (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 2880 . . . . . 6 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
21dvelimv 2502 . . . . 5 (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥𝐴 → ∀𝑦 𝑥𝐴))
3 rgen2a.1 . . . . . . 7 ((𝑥𝐴𝑦𝐴) → 𝜑)
43ex 399 . . . . . 6 (𝑥𝐴 → (𝑦𝐴𝜑))
54alimi 1896 . . . . 5 (∀𝑦 𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
62, 5syl6com 37 . . . 4 (𝑥𝐴 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦𝐴𝜑)))
7 eleq1 2880 . . . . . . 7 (𝑦 = 𝑥 → (𝑦𝐴𝑥𝐴))
87biimpd 220 . . . . . 6 (𝑦 = 𝑥 → (𝑦𝐴𝑥𝐴))
98, 4syli 39 . . . . 5 (𝑦 = 𝑥 → (𝑦𝐴𝜑))
109alimi 1896 . . . 4 (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦𝐴𝜑))
116, 10pm2.61d2 173 . . 3 (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
12 df-ral 3108 . . 3 (∀𝑦𝐴 𝜑 ↔ ∀𝑦(𝑦𝐴𝜑))
1311, 12sylibr 225 . 2 (𝑥𝐴 → ∀𝑦𝐴 𝜑)
1413rgen 3117 1 𝑥𝐴𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wal 1635  wcel 2157  wral 3103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-cleq 2806  df-clel 2809  df-ral 3108
This theorem is referenced by:  sosn  5397  isoid  6806  f1owe  6830  ordon  7215  fnwelem  7529  issmo  7684  oawordeulem  7874  ecopover  8090  unfilem2  8467  dffi2  8571  inficl  8573  fipwuni  8574  fisn  8575  dffi3  8579  cantnfvalf  8812  r111  8888  alephf1  9194  alephiso  9207  dfac5lem4  9235  kmlem9  9268  ackbij1lem17  9346  fin1a2lem2  9511  fin1a2lem4  9513  axcc2lem  9546  nqereu  10039  addpqf  10054  mulpqf  10056  genpdm  10112  axaddf  10254  axmulf  10255  subf  10571  mulnzcnopr  10961  negiso  11291  cnref1o  12044  xaddf  12276  xmulf  12323  ioof  12493  om2uzf1oi  12979  om2uzisoi  12980  wwlktovf1  13928  reeff1  15073  divalglem9  15347  bitsf1  15390  gcdf  15456  eucalgf  15518  qredeu  15593  1arith  15851  vdwapf  15896  catideu  16543  sscres  16690  fpwipodrs  17372  letsr  17435  mgmidmo  17467  frmdplusg  17599  nmznsg  17843  efgred  18365  isabli  18411  brric  18951  xrsmgm  19992  xrs1cmn  19997  xrge0subm  19998  xrsds  20000  cnsubmlem  20005  cnsubrglem  20007  nn0srg  20027  rge0srg  20028  rzgrp  20181  fibas  20999  fctop  21026  cctop  21028  iccordt  21236  fsubbas  21888  zfbas  21917  ismeti  22347  dscmet  22594  qtopbaslem  22779  tgqioo  22820  xrsxmet  22829  xrsdsre  22830  retopconn  22849  iccconn  22850  iimulcn  22954  icopnfhmeo  22959  iccpnfhmeo  22961  xrhmeo  22962  iundisj2  23536  reefiso  24422  recosf1o  24502  ercgrg  25632  2wspmdisj  27518  isabloi  27740  cncph  28008  hvsubf  28206  hhip  28368  hhph  28369  helch  28434  hsn0elch  28439  hhssabloilem  28452  hhshsslem2  28459  shscli  28510  shintcli  28522  pjmf1  28909  idunop  29171  idhmop  29175  0hmop  29176  adj0  29187  lnopunii  29205  lnophmi  29211  riesz4i  29256  cnlnadjlem9  29268  adjcoi  29293  bra11  29301  pjhmopi  29339  iundisj2f  29734  iundisj2fi  29889  xrstos  30010  xrge0omnd  30042  reofld  30171  xrge0slmod  30175  iistmd  30279  cnre2csqima  30288  mndpluscn  30303  raddcn  30306  xrge0iifiso  30312  xrge0iifmhm  30316  xrge0pluscn  30317  br2base  30662  sxbrsiga  30683  signswmnd  30965  indispconn  31544  ioosconn  31557  soseq  32080  f1omptsnlem  33502  isbasisrelowl  33524  poimirlem27  33751  exidu1  33968  rngoideu  34015  isomliN  35021  idlaut  35878  mzpclall  37793  kelac2lem  38136  clsk1indlem3  38842  icof  39899  prmdvdsfmtnof1  42075  sprsymrelf1  42315  uspgrsprf1  42324  plusfreseq  42341  nnsgrpmgm  42385  nnsgrp  42386  2zrngamgm  42508  2zrngmmgm  42515
  Copyright terms: Public domain W3C validator