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

Theorem cbvab 2564
Description: Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
Hypotheses
Ref Expression
cbvab.1  |-  F/ y
ph
cbvab.2  |-  F/ x ps
cbvab.3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvab  |-  { x  |  ph }  =  {
y  |  ps }

Proof of Theorem cbvab
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 cbvab.1 . . . . 5  |-  F/ y
ph
21sbco2 2210 . . . 4  |-  ( [ z  /  y ] [ y  /  x ] ph  <->  [ z  /  x ] ph )
3 cbvab.2 . . . . . 6  |-  F/ x ps
4 cbvab.3 . . . . . 6  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
53, 4sbie 2203 . . . . 5  |-  ( [ y  /  x ] ph 
<->  ps )
65sbbii 1794 . . . 4  |-  ( [ z  /  y ] [ y  /  x ] ph  <->  [ z  /  y ] ps )
72, 6bitr3i 255 . . 3  |-  ( [ z  /  x ] ph 
<->  [ z  /  y ] ps )
8 df-clab 2409 . . 3  |-  ( z  e.  { x  | 
ph }  <->  [ z  /  x ] ph )
9 df-clab 2409 . . 3  |-  ( z  e.  { y  |  ps }  <->  [ z  /  y ] ps )
107, 8, 93bitr4i 281 . 2  |-  ( z  e.  { x  | 
ph }  <->  z  e.  { y  |  ps }
)
1110eqriv 2419 1  |-  { x  |  ph }  =  {
y  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1438   F/wnf 1664   [wsb 1787    e. wcel 1869   {cab 2408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415
This theorem is referenced by:  cbvabv  2566  cbvrab  3080  cbvsbc  3329  cbvrabcsf  3431  rabsnifsb  4066  rabasiun  4301  dfdmf  5045  dfrnf  5090  funfv2f  5948  abrexex2g  6782  abrexex2  6786  bnj873  29737  ptrest  31859  poimirlem26  31886  poimirlem27  31887
  Copyright terms: Public domain W3C validator