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

Theorem cbvrabv 2748
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.)
Hypothesis
Ref Expression
cbvrabv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrabv  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Distinct variable groups:    x, y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvrabv
StepHypRef Expression
1 nfcv 2329 . 2  |-  F/_ x A
2 nfcv 2329 . 2  |-  F/_ y A
3 nfv 1538 . 2  |-  F/ y
ph
4 nfv 1538 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 2747 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    = wceq 1363   {crab 2469
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rab 2474
This theorem is referenced by:  pwnss  4171  acexmidlemv  5886  exmidac  7222  genipv  7522  ltexpri  7626  suplocsrlempr  7820  suplocsr  7822  zsupssdc  11969  sqne2sq  12191  eulerth  12247  odzval  12255  pcprecl  12303  pcprendvds  12304  pcpremul  12307  pceulem  12308
  Copyright terms: Public domain W3C validator