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

Theorem cbvrab 3104
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 2615 . . . . 5  |-  F/ x  z  e.  A
4 nfs1v 2157 . . . . 5  |-  F/ x [ z  /  x ] ph
53, 4nfan 1870 . . . 4  |-  F/ x
( z  e.  A  /\  [ z  /  x ] ph )
6 eleq1 2532 . . . . 5  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
7 sbequ12 1954 . . . . 5  |-  ( x  =  z  ->  ( ph 
<->  [ z  /  x ] ph ) )
86, 7anbi12d 710 . . . 4  |-  ( x  =  z  ->  (
( x  e.  A  /\  ph )  <->  ( z  e.  A  /\  [ z  /  x ] ph ) ) )
91, 5, 8cbvab 2601 . . 3  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }
10 cbvrab.2 . . . . . 6  |-  F/_ y A
1110nfcri 2615 . . . . 5  |-  F/ y  z  e.  A
12 cbvrab.3 . . . . . 6  |-  F/ y
ph
1312nfsb 2161 . . . . 5  |-  F/ y [ z  /  x ] ph
1411, 13nfan 1870 . . . 4  |-  F/ y ( z  e.  A  /\  [ z  /  x ] ph )
15 nfv 1678 . . . 4  |-  F/ z ( y  e.  A  /\  ps )
16 eleq1 2532 . . . . 5  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
17 sbequ 2083 . . . . . 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 2116 . . . . . 6  |-  ( [ y  /  x ] ph 
<->  ps )
2117, 20syl6bb 261 . . . . 5  |-  ( z  =  y  ->  ( [ z  /  x ] ph  <->  ps ) )
2216, 21anbi12d 710 . . . 4  |-  ( z  =  y  ->  (
( z  e.  A  /\  [ z  /  x ] ph )  <->  ( y  e.  A  /\  ps )
) )
2314, 15, 22cbvab 2601 . . 3  |-  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }  =  {
y  |  ( y  e.  A  /\  ps ) }
249, 23eqtri 2489 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { y  |  ( y  e.  A  /\  ps ) }
25 df-rab 2816 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
26 df-rab 2816 . 2  |-  { y  e.  A  |  ps }  =  { y  |  ( y  e.  A  /\  ps ) }
2724, 25, 263eqtr4i 2499 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1374   F/wnf 1594   [wsb 1706    e. wcel 1762   {cab 2445   F/_wnfc 2608   {crab 2811
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 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rab 2816
This theorem is referenced by:  cbvrabv  3105  elrabsf  3363  tfis  6660  cantnflem1  8097  scottexs  8294  scott0s  8295  elmptrab  20056  suppss2f  27136  scottexf  30167  scott0f  30168  eq0rabdioph  30301  rexrabdioph  30318  rexfrabdioph  30319  elnn0rabdioph  30327  dvdsrabdioph  30334  limcperiod  31125  stoweidlem34  31289  stoweidlem59  31314  fourierdlem81  31443  fourierdlem92  31454  bnj1534  32865
  Copyright terms: Public domain W3C validator