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

Theorem cbvrab 2786
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 1605 . . . 4  |-  F/ z ( x  e.  A  /\  ph )
2 cbvrab.1 . . . . . 6  |-  F/_ x A
32nfcri 2413 . . . . 5  |-  F/ x  z  e.  A
4 nfs1v 2045 . . . . 5  |-  F/ x [ z  /  x ] ph
53, 4nfan 1771 . . . 4  |-  F/ x
( z  e.  A  /\  [ z  /  x ] ph )
6 eleq1 2343 . . . . 5  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
7 sbequ12 1860 . . . . 5  |-  ( x  =  z  ->  ( ph 
<->  [ z  /  x ] ph ) )
86, 7anbi12d 691 . . . 4  |-  ( x  =  z  ->  (
( x  e.  A  /\  ph )  <->  ( z  e.  A  /\  [ z  /  x ] ph ) ) )
91, 5, 8cbvab 2401 . . 3  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }
10 cbvrab.2 . . . . . 6  |-  F/_ y A
1110nfcri 2413 . . . . 5  |-  F/ y  z  e.  A
12 cbvrab.3 . . . . . 6  |-  F/ y
ph
1312nfsb 2048 . . . . 5  |-  F/ y [ z  /  x ] ph
1411, 13nfan 1771 . . . 4  |-  F/ y ( z  e.  A  /\  [ z  /  x ] ph )
15 nfv 1605 . . . 4  |-  F/ z ( y  e.  A  /\  ps )
16 eleq1 2343 . . . . 5  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
17 sbequ 2000 . . . . . 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 1978 . . . . . 6  |-  ( [ y  /  x ] ph 
<->  ps )
2117, 20syl6bb 252 . . . . 5  |-  ( z  =  y  ->  ( [ z  /  x ] ph  <->  ps ) )
2216, 21anbi12d 691 . . . 4  |-  ( z  =  y  ->  (
( z  e.  A  /\  [ z  /  x ] ph )  <->  ( y  e.  A  /\  ps )
) )
2314, 15, 22cbvab 2401 . . 3  |-  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }  =  {
y  |  ( y  e.  A  /\  ps ) }
249, 23eqtri 2303 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { y  |  ( y  e.  A  /\  ps ) }
25 df-rab 2552 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
26 df-rab 2552 . 2  |-  { y  e.  A  |  ps }  =  { y  |  ( y  e.  A  /\  ps ) }
2724, 25, 263eqtr4i 2313 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   F/wnf 1531    = wceq 1623   [wsb 1629    e. wcel 1684   {cab 2269   F/_wnfc 2406   {crab 2547
This theorem is referenced by:  cbvrabv  2787  elrabsf  3029  tfis  4645  scottexs  7557  scott0s  7558  elmptrab  17522  ballotlemelo  23046  ballotleme  23055  suppss2f  23201  eq0rabdioph  26856  rexrabdioph  26875  rexfrabdioph  26876  elnn0rabdioph  26884  dvdsrabdioph  26891  stoweidlem34  27783  stoweidlem49  27798  stoweidlem59  27808  bnj1534  28885
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