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

Theorem rgen2a 2531
Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2017. Usage of rgen2 2563 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 1528 . . . . 5 𝑦 𝑧𝐴
2 eleq1 2240 . . . . 5 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
31, 2dvelimor 2018 . . . 4 (∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥𝐴)
4 eleq1 2240 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑦𝐴𝑥𝐴))
5 rgen2a.1 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴) → 𝜑)
65ex 115 . . . . . . . . 9 (𝑥𝐴 → (𝑦𝐴𝜑))
74, 6syl6bi 163 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦𝐴 → (𝑦𝐴𝜑)))
87pm2.43d 50 . . . . . . 7 (𝑦 = 𝑥 → (𝑦𝐴𝜑))
98alimi 1455 . . . . . 6 (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦𝐴𝜑))
109a1d 22 . . . . 5 (∀𝑦 𝑦 = 𝑥 → (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑)))
11 nfr 1518 . . . . . 6 (Ⅎ𝑦 𝑥𝐴 → (𝑥𝐴 → ∀𝑦 𝑥𝐴))
126alimi 1455 . . . . . 6 (∀𝑦 𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
1311, 12syl6 33 . . . . 5 (Ⅎ𝑦 𝑥𝐴 → (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑)))
1410, 13jaoi 716 . . . 4 ((∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥𝐴) → (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑)))
153, 14ax-mp 5 . . 3 (𝑥𝐴 → ∀𝑦(𝑦𝐴𝜑))
16 df-ral 2460 . . 3 (∀𝑦𝐴 𝜑 ↔ ∀𝑦(𝑦𝐴𝜑))
1715, 16sylibr 134 . 2 (𝑥𝐴 → ∀𝑦𝐴 𝜑)
1817rgen 2530 1 𝑥𝐴𝑦𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wo 708  wal 1351   = wceq 1353  wnf 1460  wcel 2148  wral 2455
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-ral 2460
This theorem is referenced by:  ordsucunielexmid  4531  onintexmid  4573  isoid  5811  issmo  6289  oawordriexmid  6471  ecopover  6633  ecopoverg  6636  1domsn  6819  unfiexmid  6917  axaddf  7867  axmulf  7868  subf  8159  negiso  8912  cnref1o  9650  xaddf  9844  ioof  9971  fzof  10144  xrnegiso  11270  reeff1  11708  gcdf  11973  eucalgf  12055  qredeu  12097  qnnen  12432  strsetsid  12495  hmeofn  13805  ismeti  13849  qtopbasss  14024  tgqioo  14050  peano4nninf  14758
  Copyright terms: Public domain W3C validator