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

Theorem rgen2a 2429
Description: Generalization rule for restricted quantification. Note that  x and  y needn't be distinct (and illustrates the use of dvelimor 1942). (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.)
Hypothesis
Ref Expression
rgen2a.1  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ph )
Assertion
Ref Expression
rgen2a  |-  A. x  e.  A  A. y  e.  A  ph
Distinct variable group:    y, A
Allowed substitution hints:    ph( x, y)    A( x)

Proof of Theorem rgen2a
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 nfv 1466 . . . . 5  |-  F/ y  z  e.  A
2 eleq1 2150 . . . . 5  |-  ( z  =  x  ->  (
z  e.  A  <->  x  e.  A ) )
31, 2dvelimor 1942 . . . 4  |-  ( A. y  y  =  x  \/  F/ y  x  e.  A )
4 eleq1 2150 . . . . . . . . 9  |-  ( y  =  x  ->  (
y  e.  A  <->  x  e.  A ) )
5 rgen2a.1 . . . . . . . . . 10  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ph )
65ex 113 . . . . . . . . 9  |-  ( x  e.  A  ->  (
y  e.  A  ->  ph ) )
74, 6syl6bi 161 . . . . . . . 8  |-  ( y  =  x  ->  (
y  e.  A  -> 
( y  e.  A  ->  ph ) ) )
87pm2.43d 49 . . . . . . 7  |-  ( y  =  x  ->  (
y  e.  A  ->  ph ) )
98alimi 1389 . . . . . 6  |-  ( A. y  y  =  x  ->  A. y ( y  e.  A  ->  ph )
)
109a1d 22 . . . . 5  |-  ( A. y  y  =  x  ->  ( x  e.  A  ->  A. y ( y  e.  A  ->  ph )
) )
11 nfr 1456 . . . . . 6  |-  ( F/ y  x  e.  A  ->  ( x  e.  A  ->  A. y  x  e.  A ) )
126alimi 1389 . . . . . 6  |-  ( A. y  x  e.  A  ->  A. y ( y  e.  A  ->  ph )
)
1311, 12syl6 33 . . . . 5  |-  ( F/ y  x  e.  A  ->  ( x  e.  A  ->  A. y ( y  e.  A  ->  ph )
) )
1410, 13jaoi 671 . . . 4  |-  ( ( A. y  y  =  x  \/  F/ y  x  e.  A )  ->  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) ) )
153, 14ax-mp 7 . . 3  |-  ( x  e.  A  ->  A. y
( y  e.  A  ->  ph ) )
16 df-ral 2364 . . 3  |-  ( A. y  e.  A  ph  <->  A. y
( y  e.  A  ->  ph ) )
1715, 16sylibr 132 . 2  |-  ( x  e.  A  ->  A. y  e.  A  ph )
1817rgen 2428 1  |-  A. x  e.  A  A. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    \/ wo 664   A.wal 1287    = wceq 1289   F/wnf 1394    e. wcel 1438   A.wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-cleq 2081  df-clel 2084  df-ral 2364
This theorem is referenced by:  ordsucunielexmid  4337  onintexmid  4378  isoid  5571  issmo  6035  oawordriexmid  6213  ecopover  6370  ecopoverg  6373  1domsn  6515  unfiexmid  6608  subf  7663  negiso  8388  cnref1o  9102  ioof  9358  fzof  9520  gcdf  11046  eucalgf  11119  qredeu  11161  peano4nninf  11542
  Copyright terms: Public domain W3C validator