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

Theorem cbvrab 3093
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 1694 . . . 4  |-  F/ z ( x  e.  A  /\  ph )
2 cbvrab.1 . . . . . 6  |-  F/_ x A
32nfcri 2598 . . . . 5  |-  F/ x  z  e.  A
4 nfs1v 2167 . . . . 5  |-  F/ x [ z  /  x ] ph
53, 4nfan 1914 . . . 4  |-  F/ x
( z  e.  A  /\  [ z  /  x ] ph )
6 eleq1 2515 . . . . 5  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
7 sbequ12 1978 . . . . 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 2584 . . 3  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }
10 cbvrab.2 . . . . . 6  |-  F/_ y A
1110nfcri 2598 . . . . 5  |-  F/ y  z  e.  A
12 cbvrab.3 . . . . . 6  |-  F/ y
ph
1312nfsb 2170 . . . . 5  |-  F/ y [ z  /  x ] ph
1411, 13nfan 1914 . . . 4  |-  F/ y ( z  e.  A  /\  [ z  /  x ] ph )
15 nfv 1694 . . . 4  |-  F/ z ( y  e.  A  /\  ps )
16 eleq1 2515 . . . . 5  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
17 sbequ 2103 . . . . . 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 2135 . . . . . 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 2584 . . 3  |-  { z  |  ( z  e.  A  /\  [ z  /  x ] ph ) }  =  {
y  |  ( y  e.  A  /\  ps ) }
249, 23eqtri 2472 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { y  |  ( y  e.  A  /\  ps ) }
25 df-rab 2802 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
26 df-rab 2802 . 2  |-  { y  e.  A  |  ps }  =  { y  |  ( y  e.  A  /\  ps ) }
2724, 25, 263eqtr4i 2482 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383   F/wnf 1603   [wsb 1726    e. wcel 1804   {cab 2428   F/_wnfc 2591   {crab 2797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802
This theorem is referenced by:  cbvrabv  3094  elrabsf  3352  tfis  6674  cantnflem1  8111  scottexs  8308  scott0s  8309  elmptrab  20201  suppss2f  27349  scottexf  30551  scott0f  30552  eq0rabdioph  30685  rexrabdioph  30702  rexfrabdioph  30703  elnn0rabdioph  30711  dvdsrabdioph  30718  stoweidlem34  31705  stoweidlem59  31730  bnj1534  33644
  Copyright terms: Public domain W3C validator