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

Theorem sbceqg 3975
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 3432 . . 3 (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝐵 = 𝐶[𝐴 / 𝑥]𝐵 = 𝐶))
2 dfsbcq2 3432 . . . . 5 (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦𝐵[𝐴 / 𝑥]𝑦𝐵))
32abbidv 2739 . . . 4 (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐵})
4 dfsbcq2 3432 . . . . 5 (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐶))
54abbidv 2739 . . . 4 (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶} = {𝑦[𝐴 / 𝑥]𝑦𝐶})
63, 5eqeq12d 2635 . . 3 (𝑧 = 𝐴 → ({𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶} ↔ {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶}))
7 nfs1v 2435 . . . . . 6 𝑥[𝑧 / 𝑥]𝑦𝐵
87nfab 2766 . . . . 5 𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵}
9 nfs1v 2435 . . . . . 6 𝑥[𝑧 / 𝑥]𝑦𝐶
109nfab 2766 . . . . 5 𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶}
118, 10nfeq 2773 . . . 4 𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶}
12 sbab 2748 . . . . 5 (𝑥 = 𝑧𝐵 = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵})
13 sbab 2748 . . . . 5 (𝑥 = 𝑧𝐶 = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶})
1412, 13eqeq12d 2635 . . . 4 (𝑥 = 𝑧 → (𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶}))
1511, 14sbie 2406 . . 3 ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶})
161, 6, 15vtoclbg 3262 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶}))
17 df-csb 3527 . . 3 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
18 df-csb 3527 . . 3 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
1917, 18eqeq12i 2634 . 2 (𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶 ↔ {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶})
2016, 19syl6bbr 278 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  [wsb 1878  wcel 1988  {cab 2606  [wsbc 3429  csb 3526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-sbc 3430  df-csb 3527
This theorem is referenced by:  sbcne12  3977  sbceq1g  3979  sbceq2g  3981  sbcfng  6029  swrdspsleq  13431  fprodmodd  14709  csbwrecsg  33144  relowlpssretop  33183  rdgeqoa  33189  poimirlem25  33405  sbceqi  33884  cdlemk42  36048  onfrALTlem5  38577  onfrALTlem4  38578  csbeq2gOLD  38585  csbfv12gALTOLD  38872  csbingVD  38940  onfrALTlem5VD  38941  onfrALTlem4VD  38942  csbeq2gVD  38948  csbsngVD  38949  csbunigVD  38954  csbfv12gALTVD  38955
  Copyright terms: Public domain W3C validator