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  4527  onintexmid  4569  isoid  5805  issmo  6283  oawordriexmid  6465  ecopover  6627  ecopoverg  6630  1domsn  6813  unfiexmid  6911  axaddf  7855  axmulf  7856  subf  8146  negiso  8898  cnref1o  9636  xaddf  9828  ioof  9955  fzof  10127  xrnegiso  11251  reeff1  11689  gcdf  11953  eucalgf  12035  qredeu  12077  qnnen  12412  strsetsid  12475  hmeofn  13462  ismeti  13506  qtopbasss  13681  tgqioo  13707  peano4nninf  14404
  Copyright terms: Public domain W3C validator