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

Theorem sbceqg 4333
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 3750 . . 3 (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝐵 = 𝐶[𝐴 / 𝑥]𝐵 = 𝐶))
2 dfsbcq2 3750 . . . . 5 (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦𝐵[𝐴 / 𝑥]𝑦𝐵))
32abbidv 2886 . . . 4 (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐵})
4 dfsbcq2 3750 . . . . 5 (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐶))
54abbidv 2886 . . . 4 (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶} = {𝑦[𝐴 / 𝑥]𝑦𝐶})
63, 5eqeq12d 2838 . . 3 (𝑧 = 𝐴 → ({𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶} ↔ {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶}))
7 nfs1v 2160 . . . . . 6 𝑥[𝑧 / 𝑥]𝑦𝐵
87nfab 2985 . . . . 5 𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵}
9 nfs1v 2160 . . . . . 6 𝑥[𝑧 / 𝑥]𝑦𝐶
109nfab 2985 . . . . 5 𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶}
118, 10nfeq 2992 . . . 4 𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶}
12 sbab 2959 . . . . 5 (𝑥 = 𝑧𝐵 = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵})
13 sbab 2959 . . . . 5 (𝑥 = 𝑧𝐶 = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶})
1412, 13eqeq12d 2838 . . . 4 (𝑥 = 𝑧 → (𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶}))
1511, 14sbiev 2331 . . 3 ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦𝐶})
161, 6, 15vtoclbg 3544 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶}))
17 df-csb 3856 . . 3 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
18 df-csb 3856 . . 3 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
1917, 18eqeq12i 2837 . 2 (𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶 ↔ {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦[𝐴 / 𝑥]𝑦𝐶})
2016, 19syl6bbr 292 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  [wsb 2069  wcel 2114  {cab 2800  [wsbc 3747  csb 3855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-sbc 3748  df-csb 3856
This theorem is referenced by:  sbceqi  4334  sbcne12  4336  sbceq1g  4338  sbceq2g  4340  csbie2df  4364  sbcfng  6491  swrdspsleq  14018  fprodmodd  15342  csbwrecsg  34705  relowlpssretop  34742  rdgeqoa  34748  poimirlem25  35041  cdlemk42  38196  onfrALTlem5  41183  onfrALTlem4  41184  csbingVD  41525  onfrALTlem5VD  41526  onfrALTlem4VD  41527  csbeq2gVD  41533  csbsngVD  41534  csbunigVD  41539  csbfv12gALTVD  41540
  Copyright terms: Public domain W3C validator