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

Theorem cbvrab 2968
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.)
Hypotheses
Ref Expression
cbvrab.1  |-  F/_ x A
cbvrab.2  |-  F/_ y A
cbvrab.3  |-  F/ y
ph
cbvrab.4  |-  F/ x ps
cbvrab.5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrab  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }

Proof of Theorem cbvrab
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 nfv 1678 . . . 4  |-  F/ z ( x  e.  A  /\  ph )
2 cbvrab.1 . . . . . 6  |-  F/_ x A
32nfcri 2571 . . . . 5  |-  F/ x  z  e.  A
4 nfs1v 2147 . . . . 5  |-  F/ x [ z  /  x ] ph
53, 4nfan 1865 . . . 4  |-  F/ x
( z  e.  A  /\  [ z  /  x ] ph )
6 eleq1 2501 . . . . 5  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
7 sbequ12 1941 . . . . 5  |-  ( x  =  z  ->  ( ph 
<->  [ z  /  x ] ph ) )
86, 7anbi12d 705 . . . 4  |-  ( x  =  z  ->  (
( x  e.  A  /\  ph )  <->  ( z  e.  A  /\  [ z  /  x ] ph ) ) )
91, 5, 8cbvab 2559 . . 3  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }
10 cbvrab.2 . . . . . 6  |-  F/_ y A
1110nfcri 2571 . . . . 5  |-  F/ y  z  e.  A
12 cbvrab.3 . . . . . 6  |-  F/ y
ph
1312nfsb 2151 . . . . 5  |-  F/ y [ z  /  x ] ph
1411, 13nfan 1865 . . . 4  |-  F/ y ( z  e.  A  /\  [ z  /  x ] ph )
15 nfv 1678 . . . 4  |-  F/ z ( y  e.  A  /\  ps )
16 eleq1 2501 . . . . 5  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
17 sbequ 2072 . . . . . 6  |-  ( z  =  y  ->  ( [ z  /  x ] ph  <->  [ y  /  x ] ph ) )
18 cbvrab.4 . . . . . . 7  |-  F/ x ps
19 cbvrab.5 . . . . . . 7  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
2018, 19sbie 2105 . . . . . 6  |-  ( [ y  /  x ] ph 
<->  ps )
2117, 20syl6bb 261 . . . . 5  |-  ( z  =  y  ->  ( [ z  /  x ] ph  <->  ps ) )
2216, 21anbi12d 705 . . . 4  |-  ( z  =  y  ->  (
( z  e.  A  /\  [ z  /  x ] ph )  <->  ( y  e.  A  /\  ps )
) )
2314, 15, 22cbvab 2559 . . 3  |-  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }  =  {
y  |  ( y  e.  A  /\  ps ) }
249, 23eqtri 2461 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { y  |  ( y  e.  A  /\  ps ) }
25 df-rab 2722 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
26 df-rab 2722 . 2  |-  { y  e.  A  |  ps }  =  { y  |  ( y  e.  A  /\  ps ) }
2724, 25, 263eqtr4i 2471 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364   F/wnf 1594   [wsb 1705    e. wcel 1761   {cab 2427   F/_wnfc 2564   {crab 2717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722
This theorem is referenced by:  cbvrabv  2969  elrabsf  3222  tfis  6464  cantnflem1  7893  scottexs  8090  scott0s  8091  elmptrab  19359  suppss2f  25889  scottexf  28905  scott0f  28906  eq0rabdioph  29040  rexrabdioph  29057  rexfrabdioph  29058  elnn0rabdioph  29066  dvdsrabdioph  29073  stoweidlem34  29754  stoweidlem59  29779  bnj1534  31680
  Copyright terms: Public domain W3C validator