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

Theorem cbvrab 3032
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 1715 . . . 4  |-  F/ z ( x  e.  A  /\  ph )
2 cbvrab.1 . . . . . 6  |-  F/_ x A
32nfcri 2537 . . . . 5  |-  F/ x  z  e.  A
4 nfs1v 2185 . . . . 5  |-  F/ x [ z  /  x ] ph
53, 4nfan 1936 . . . 4  |-  F/ x
( z  e.  A  /\  [ z  /  x ] ph )
6 eleq1 2454 . . . . 5  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
7 sbequ12 2000 . . . . 5  |-  ( x  =  z  ->  ( ph 
<->  [ z  /  x ] ph ) )
86, 7anbi12d 708 . . . 4  |-  ( x  =  z  ->  (
( x  e.  A  /\  ph )  <->  ( z  e.  A  /\  [ z  /  x ] ph ) ) )
91, 5, 8cbvab 2523 . . 3  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }
10 cbvrab.2 . . . . . 6  |-  F/_ y A
1110nfcri 2537 . . . . 5  |-  F/ y  z  e.  A
12 cbvrab.3 . . . . . 6  |-  F/ y
ph
1312nfsb 2188 . . . . 5  |-  F/ y [ z  /  x ] ph
1411, 13nfan 1936 . . . 4  |-  F/ y ( z  e.  A  /\  [ z  /  x ] ph )
15 nfv 1715 . . . 4  |-  F/ z ( y  e.  A  /\  ps )
16 eleq1 2454 . . . . 5  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
17 sbequ 2121 . . . . . 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 2153 . . . . . 6  |-  ( [ y  /  x ] ph 
<->  ps )
2117, 20syl6bb 261 . . . . 5  |-  ( z  =  y  ->  ( [ z  /  x ] ph  <->  ps ) )
2216, 21anbi12d 708 . . . 4  |-  ( z  =  y  ->  (
( z  e.  A  /\  [ z  /  x ] ph )  <->  ( y  e.  A  /\  ps )
) )
2314, 15, 22cbvab 2523 . . 3  |-  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }  =  {
y  |  ( y  e.  A  /\  ps ) }
249, 23eqtri 2411 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { y  |  ( y  e.  A  /\  ps ) }
25 df-rab 2741 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
26 df-rab 2741 . 2  |-  { y  e.  A  |  ps }  =  { y  |  ( y  e.  A  /\  ps ) }
2724, 25, 263eqtr4i 2421 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399   F/wnf 1624   [wsb 1747    e. wcel 1826   {cab 2367   F/_wnfc 2530   {crab 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741
This theorem is referenced by:  cbvrabv  3033  elrabsf  3291  tfis  6588  cantnflem1  8021  scottexs  8218  scott0s  8219  elmptrab  20413  suppss2f  27617  scottexf  30742  scott0f  30743  eq0rabdioph  30875  rexrabdioph  30893  rexfrabdioph  30894  elnn0rabdioph  30902  dvdsrabdioph  30909  binomcxplemdvsum  31428  stoweidlem34  31982  stoweidlem59  32007  bnj1534  34258
  Copyright terms: Public domain W3C validator