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

Theorem sbceqg 4175
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 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶))

Proof of Theorem sbceqg
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfsbcq2 3630 . . 3 (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝐵 = 𝐶[𝐴 / 𝑥]𝐵 = 𝐶))
2 dfsbcq2 3630 . . . . 5 (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦𝐵[𝐴 / 𝑥]𝑦𝐵))
32abbidv 2921 . . . 4 (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐵})
4 dfsbcq2 3630 . . . . 5 (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐶))
54abbidv 2921 . . . 4 (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶} = {𝑦[𝐴 / 𝑥]𝑦𝐶})
63, 5eqeq12d 2817 . . 3 (𝑧 = 𝐴 → ({𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶} ↔ {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶}))
7 nfs1v 2285 . . . . . 6 𝑥[𝑧 / 𝑥]𝑦𝐵
87nfab 2949 . . . . 5 𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵}
9 nfs1v 2285 . . . . . 6 𝑥[𝑧 / 𝑥]𝑦𝐶
109nfab 2949 . . . . 5 𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶}
118, 10nfeq 2956 . . . 4 𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶}
12 sbab 2930 . . . . 5 (𝑥 = 𝑧𝐵 = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵})
13 sbab 2930 . . . . 5 (𝑥 = 𝑧𝐶 = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶})
1412, 13eqeq12d 2817 . . . 4 (𝑥 = 𝑧 → (𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶}))
1511, 14sbie 2566 . . 3 ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶})
161, 6, 15vtoclbg 3456 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶}))
17 df-csb 3723 . . 3 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
18 df-csb 3723 . . 3 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
1917, 18eqeq12i 2816 . 2 (𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶 ↔ {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶})
2016, 19syl6bbr 280 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  [wsb 2059  wcel 2155  {cab 2788  [wsbc 3627  csb 3722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-sbc 3628  df-csb 3723
This theorem is referenced by:  sbcne12  4177  sbceq1g  4179  sbceq2g  4181  sbcfng  6247  swrdspsleq  13667  fprodmodd  14942  csbwrecsg  33484  relowlpssretop  33522  rdgeqoa  33528  poimirlem25  33741  sbceqi  34218  cdlemk42  36716  onfrALTlem5  39249  onfrALTlem4  39250  csbeq2gOLD  39257  csbingVD  39608  onfrALTlem5VD  39609  onfrALTlem4VD  39610  csbeq2gVD  39616  csbsngVD  39617  csbunigVD  39622  csbfv12gALTVD  39623
  Copyright terms: Public domain W3C validator