MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvrabv Unicode version

Theorem cbvrabv 2787
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 2419 . 2  |-  F/_ x A
2 nfcv 2419 . 2  |-  F/_ y A
3 nfv 1605 . 2  |-  F/ y
ph
4 nfv 1605 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 2786 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   {crab 2547
This theorem is referenced by:  pwnss  4176  knatar  5857  oeeulem  6599  ordtypecbv  7232  ordtypelem9  7241  inf3lema  7325  oemapso  7384  oemapvali  7386  tz9.12lem3  7461  cofsmo  7895  enfin2i  7947  fin23lem33  7971  isf32lem11  7989  zorn2g  8130  pwfseqlem1  8280  pwfseqlem3  8282  zsupss  10307  zmin  10312  reexALT  10348  hashbc  11391  sqrlem7  11734  rpnnen  12505  divalglem5  12596  bitsfzolem  12625  smupp1  12671  gcdcllem3  12692  bezout  12721  eulerth  12851  odzval  12856  pcprecl  12892  pcprendvds  12893  pcpremul  12896  pceulem  12898  prmreclem1  12963  prmreclem5  12967  prmreclem6  12968  4sqlem19  13010  vdwnn  13045  hashbcval  13049  gsumvalx  14451  efgsdm  15039  efgsfo  15048  ablfaclem3  15322  ltbwe  16214  coe1mul2lem2  16345  pptbas  16745  concompss  17159  ptcmplem5  17750  icccmplem2  18328  minveclem5  18797  ivth  18814  ovolicc2lem5  18880  ovolicc  18882  opnmbllem  18956  vitali  18968  itg2monolem3  19107  elqaa  19702  radcnvle  19796  pserdvlem2  19804  wilth  20309  ftalem6  20315  ubthlem3  21451  htth  21498  ballotlem7  23094  subfacp1lem6  23716  erdsze  23733  cvmscbv  23789  cvmsiota  23808  cvmlift2lem13  23846  axcontlem11  24602  neibastop2  26310  eldioph4i  26895  lclkrs2  31730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552
  Copyright terms: Public domain W3C validator