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

Theorem sbceqg 3269
Description: Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Assertion
Ref Expression
sbceqg  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  =  C  <->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) )

Proof of Theorem sbceqg
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfsbcq2 3166 . . 3  |-  ( z  =  A  ->  ( [ z  /  x ] B  =  C  <->  [. A  /  x ]. B  =  C )
)
2 dfsbcq2 3166 . . . . 5  |-  ( z  =  A  ->  ( [ z  /  x ] y  e.  B  <->  [. A  /  x ]. y  e.  B )
)
32abbidv 2552 . . . 4  |-  ( z  =  A  ->  { y  |  [ z  /  x ] y  e.  B }  =  { y  |  [. A  /  x ]. y  e.  B } )
4 dfsbcq2 3166 . . . . 5  |-  ( z  =  A  ->  ( [ z  /  x ] y  e.  C  <->  [. A  /  x ]. y  e.  C )
)
54abbidv 2552 . . . 4  |-  ( z  =  A  ->  { y  |  [ z  /  x ] y  e.  C }  =  { y  |  [. A  /  x ]. y  e.  C } )
63, 5eqeq12d 2452 . . 3  |-  ( z  =  A  ->  ( { y  |  [
z  /  x ]
y  e.  B }  =  { y  |  [
z  /  x ]
y  e.  C }  <->  { y  |  [. A  /  x ]. y  e.  B }  =  {
y  |  [. A  /  x ]. y  e.  C } ) )
7 nfs1v 2184 . . . . . 6  |-  F/ x [ z  /  x ] y  e.  B
87nfab 2578 . . . . 5  |-  F/_ x { y  |  [
z  /  x ]
y  e.  B }
9 nfs1v 2184 . . . . . 6  |-  F/ x [ z  /  x ] y  e.  C
109nfab 2578 . . . . 5  |-  F/_ x { y  |  [
z  /  x ]
y  e.  C }
118, 10nfeq 2581 . . . 4  |-  F/ x { y  |  [
z  /  x ]
y  e.  B }  =  { y  |  [
z  /  x ]
y  e.  C }
12 sbab 2560 . . . . 5  |-  ( x  =  z  ->  B  =  { y  |  [
z  /  x ]
y  e.  B }
)
13 sbab 2560 . . . . 5  |-  ( x  =  z  ->  C  =  { y  |  [
z  /  x ]
y  e.  C }
)
1412, 13eqeq12d 2452 . . . 4  |-  ( x  =  z  ->  ( B  =  C  <->  { y  |  [ z  /  x ] y  e.  B }  =  { y  |  [ z  /  x ] y  e.  C } ) )
1511, 14sbie 2151 . . 3  |-  ( [ z  /  x ] B  =  C  <->  { y  |  [ z  /  x ] y  e.  B }  =  { y  |  [ z  /  x ] y  e.  C } )
161, 6, 15vtoclbg 3014 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  =  C  <->  { y  |  [. A  /  x ]. y  e.  B }  =  {
y  |  [. A  /  x ]. y  e.  C } ) )
17 df-csb 3254 . . 3  |-  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
18 df-csb 3254 . . 3  |-  [_ A  /  x ]_ C  =  { y  |  [. A  /  x ]. y  e.  C }
1917, 18eqeq12i 2451 . 2  |-  ( [_ A  /  x ]_ B  =  [_ A  /  x ]_ C  <->  { y  |  [. A  /  x ]. y  e.  B }  =  {
y  |  [. A  /  x ]. y  e.  C } )
2016, 19syl6bbr 256 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  =  C  <->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   [wsb 1659    e. wcel 1726   {cab 2424   [.wsbc 3163   [_csb 3253
This theorem is referenced by:  sbcne12g  3271  sbceq1g  3273  sbceq2g  3275  csbfv12gALT  5741  onfrALTlem5  28630  onfrALTlem4  28631  csbeq2g  28638  csbingVD  28998  onfrALTlem5VD  28999  onfrALTlem4VD  29000  csbeq2gVD  29006  csbsngVD  29007  csbunigVD  29012  csbfv12gALTVD  29013  cdlemk42  31740
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-sbc 3164  df-csb 3254
  Copyright terms: Public domain W3C validator