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

Theorem sbceqg 3785
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 3282 . . 3  |-  ( z  =  A  ->  ( [ z  /  x ] B  =  C  <->  [. A  /  x ]. B  =  C )
)
2 dfsbcq2 3282 . . . . 5  |-  ( z  =  A  ->  ( [ z  /  x ] y  e.  B  <->  [. A  /  x ]. y  e.  B )
)
32abbidv 2580 . . . 4  |-  ( z  =  A  ->  { y  |  [ z  /  x ] y  e.  B }  =  { y  |  [. A  /  x ]. y  e.  B } )
4 dfsbcq2 3282 . . . . 5  |-  ( z  =  A  ->  ( [ z  /  x ] y  e.  C  <->  [. A  /  x ]. y  e.  C )
)
54abbidv 2580 . . . 4  |-  ( z  =  A  ->  { y  |  [ z  /  x ] y  e.  C }  =  { y  |  [. A  /  x ]. y  e.  C } )
63, 5eqeq12d 2477 . . 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 2277 . . . . . 6  |-  F/ x [ z  /  x ] y  e.  B
87nfab 2607 . . . . 5  |-  F/_ x { y  |  [
z  /  x ]
y  e.  B }
9 nfs1v 2277 . . . . . 6  |-  F/ x [ z  /  x ] y  e.  C
109nfab 2607 . . . . 5  |-  F/_ x { y  |  [
z  /  x ]
y  e.  C }
118, 10nfeq 2614 . . . 4  |-  F/ x { y  |  [
z  /  x ]
y  e.  B }  =  { y  |  [
z  /  x ]
y  e.  C }
12 sbab 2589 . . . . 5  |-  ( x  =  z  ->  B  =  { y  |  [
z  /  x ]
y  e.  B }
)
13 sbab 2589 . . . . 5  |-  ( x  =  z  ->  C  =  { y  |  [
z  /  x ]
y  e.  C }
)
1412, 13eqeq12d 2477 . . . 4  |-  ( x  =  z  ->  ( B  =  C  <->  { y  |  [ z  /  x ] y  e.  B }  =  { y  |  [ z  /  x ] y  e.  C } ) )
1511, 14sbie 2248 . . 3  |-  ( [ z  /  x ] B  =  C  <->  { y  |  [ z  /  x ] y  e.  B }  =  { y  |  [ z  /  x ] y  e.  C } )
161, 6, 15vtoclbg 3120 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  =  C  <->  { y  |  [. A  /  x ]. y  e.  B }  =  {
y  |  [. A  /  x ]. y  e.  C } ) )
17 df-csb 3376 . . 3  |-  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
18 df-csb 3376 . . 3  |-  [_ A  /  x ]_ C  =  { y  |  [. A  /  x ]. y  e.  C }
1917, 18eqeq12i 2476 . 2  |-  ( [_ A  /  x ]_ B  =  [_ A  /  x ]_ C  <->  { y  |  [. A  /  x ]. y  e.  B }  =  {
y  |  [. A  /  x ]. y  e.  C } )
2016, 19syl6bbr 271 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  =  C  <->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1455   [wsb 1808    e. wcel 1898   {cab 2448   [.wsbc 3279   [_csb 3375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-sbc 3280  df-csb 3376
This theorem is referenced by:  sbcne12  3787  sbceq1g  3789  sbceq2g  3791  sbcfng  5752  swrdspsleq  12848  csbwrecsg  31774  relowlpssretop  31813  rdgeqoa  31819  poimirlem25  32011  sbceqi  32394  cdlemk42  34554  onfrALTlem5  36953  onfrALTlem4  36954  csbeq2gOLD  36961  csbfv12gALTOLD  37254  csbingVD  37322  onfrALTlem5VD  37323  onfrALTlem4VD  37324  csbeq2gVD  37330  csbsngVD  37331  csbunigVD  37336  csbfv12gALTVD  37337
  Copyright terms: Public domain W3C validator