ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rgen2a GIF version

Theorem rgen2a 2544
Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2029. Usage of rgen2 2576 instead is highly encouraged. (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.) (New usage 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 nfv 1539 . . . . 5 𝑦 𝑧𝐴
2 eleq1 2252 . . . . 5 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
31, 2dvelimor 2030 . . . 4 (∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥𝐴)
4 eleq1 2252 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑦𝐴𝑥𝐴))
5 rgen2a.1 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴) → 𝜑)
65ex 115 . . . . . . . . 9 (𝑥𝐴 → (𝑦𝐴𝜑))
74, 6biimtrdi 163 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦𝐴 → (𝑦𝐴𝜑)))
87pm2.43d 50 . . . . . . 7 (𝑦 = 𝑥 → (𝑦𝐴𝜑))
98alimi 1466 . . . . . 6 (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦𝐴𝜑))
109a1d 22 . . . . 5 (∀𝑦 𝑦 = 𝑥 → (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑)))
11 nfr 1529 . . . . . 6 (Ⅎ𝑦 𝑥𝐴 → (𝑥𝐴 → ∀𝑦 𝑥𝐴))
126alimi 1466 . . . . . 6 (∀𝑦 𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
1311, 12syl6 33 . . . . 5 (Ⅎ𝑦 𝑥𝐴 → (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑)))
1410, 13jaoi 717 . . . 4 ((∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥𝐴) → (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑)))
153, 14ax-mp 5 . . 3 (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
16 df-ral 2473 . . 3 (∀𝑦𝐴 𝜑 ↔ ∀𝑦(𝑦𝐴𝜑))
1715, 16sylibr 134 . 2 (𝑥𝐴 → ∀𝑦𝐴 𝜑)
1817rgen 2543 1 𝑥𝐴𝑦𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wo 709  wal 1362   = wceq 1364  wnf 1471  wcel 2160  wral 2468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-cleq 2182  df-clel 2185  df-ral 2473
This theorem is referenced by:  ordsucunielexmid  4548  onintexmid  4590  isoid  5832  issmo  6314  oawordriexmid  6496  ecopover  6660  ecopoverg  6663  1domsn  6846  unfiexmid  6947  axaddf  7898  axmulf  7899  subf  8190  negiso  8943  cnref1o  9682  xaddf  9876  ioof  10003  fzof  10176  xrnegiso  11305  reeff1  11743  gcdf  12008  eucalgf  12090  qredeu  12132  qnnen  12485  strsetsid  12548  hmeofn  14279  ismeti  14323  qtopbasss  14498  tgqioo  14524  peano4nninf  15234
  Copyright terms: Public domain W3C validator