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

Theorem csbie2df 4380
Description: Conversion of implicit substitution to explicit class substitution. This version of csbiedf 3868 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. Deduction form of csbie2 3879. (Contributed by AV, 29-Mar-2024.)
Hypotheses
Ref Expression
csbie2df.p 𝑥𝜑
csbie2df.c (𝜑𝑥𝐶)
csbie2df.d (𝜑𝑥𝐷)
csbie2df.a (𝜑𝐴𝑉)
csbie2df.1 ((𝜑𝑥 = 𝑦) → 𝐵 = 𝐶)
csbie2df.2 ((𝜑𝑦 = 𝐴) → 𝐶 = 𝐷)
Assertion
Ref Expression
csbie2df (𝜑𝐴 / 𝑥𝐵 = 𝐷)
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵   𝑦,𝐷   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥,𝑦)   𝐷(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem csbie2df
StepHypRef Expression
1 csbie2df.a . 2 (𝜑𝐴𝑉)
2 eqidd 2741 . . 3 (𝜑𝐷 = 𝐷)
3 dfsbcq 3722 . . . . . 6 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝐵 = 𝐷[𝐴 / 𝑥]𝐵 = 𝐷))
4 sbceqg 4349 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐷))
54adantr 481 . . . . . . . 8 ((𝐴𝑉𝜑) → ([𝐴 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐷))
6 csbie2df.d . . . . . . . . . 10 (𝜑𝑥𝐷)
7 csbtt 3854 . . . . . . . . . 10 ((𝐴𝑉𝑥𝐷) → 𝐴 / 𝑥𝐷 = 𝐷)
86, 7sylan2 593 . . . . . . . . 9 ((𝐴𝑉𝜑) → 𝐴 / 𝑥𝐷 = 𝐷)
98eqeq2d 2751 . . . . . . . 8 ((𝐴𝑉𝜑) → (𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐷𝐴 / 𝑥𝐵 = 𝐷))
105, 9bitrd 278 . . . . . . 7 ((𝐴𝑉𝜑) → ([𝐴 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐷))
111, 10mpancom 685 . . . . . 6 (𝜑 → ([𝐴 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐷))
123, 11sylan9bb 510 . . . . 5 ((𝑦 = 𝐴𝜑) → ([𝑦 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐷))
1312pm5.74da 801 . . . 4 (𝑦 = 𝐴 → ((𝜑[𝑦 / 𝑥]𝐵 = 𝐷) ↔ (𝜑𝐴 / 𝑥𝐵 = 𝐷)))
14 csbie2df.2 . . . . . . 7 ((𝜑𝑦 = 𝐴) → 𝐶 = 𝐷)
1514eqeq1d 2742 . . . . . 6 ((𝜑𝑦 = 𝐴) → (𝐶 = 𝐷𝐷 = 𝐷))
1615expcom 414 . . . . 5 (𝑦 = 𝐴 → (𝜑 → (𝐶 = 𝐷𝐷 = 𝐷)))
1716pm5.74d 272 . . . 4 (𝑦 = 𝐴 → ((𝜑𝐶 = 𝐷) ↔ (𝜑𝐷 = 𝐷)))
18 sbsbc 3724 . . . . . 6 ([𝑦 / 𝑥]𝐵 = 𝐷[𝑦 / 𝑥]𝐵 = 𝐷)
19 csbie2df.p . . . . . . 7 𝑥𝜑
20 csbie2df.c . . . . . . . 8 (𝜑𝑥𝐶)
2120, 6nfeqd 2919 . . . . . . 7 (𝜑 → Ⅎ𝑥 𝐶 = 𝐷)
22 csbie2df.1 . . . . . . . . 9 ((𝜑𝑥 = 𝑦) → 𝐵 = 𝐶)
2322eqeq1d 2742 . . . . . . . 8 ((𝜑𝑥 = 𝑦) → (𝐵 = 𝐷𝐶 = 𝐷))
2423ex 413 . . . . . . 7 (𝜑 → (𝑥 = 𝑦 → (𝐵 = 𝐷𝐶 = 𝐷)))
2519, 21, 24sbiedw 2314 . . . . . 6 (𝜑 → ([𝑦 / 𝑥]𝐵 = 𝐷𝐶 = 𝐷))
2618, 25bitr3id 285 . . . . 5 (𝜑 → ([𝑦 / 𝑥]𝐵 = 𝐷𝐶 = 𝐷))
2726pm5.74i 270 . . . 4 ((𝜑[𝑦 / 𝑥]𝐵 = 𝐷) ↔ (𝜑𝐶 = 𝐷))
2813, 17, 27vtoclbg 3506 . . 3 (𝐴𝑉 → ((𝜑𝐴 / 𝑥𝐵 = 𝐷) ↔ (𝜑𝐷 = 𝐷)))
292, 28mpbiri 257 . 2 (𝐴𝑉 → (𝜑𝐴 / 𝑥𝐵 = 𝐷))
301, 29mpcom 38 1 (𝜑𝐴 / 𝑥𝐵 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1542  wnf 1790  [wsb 2071  wcel 2110  wnfc 2889  [wsbc 3720  csb 3837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-sbc 3721  df-csb 3838
This theorem is referenced by:  fvmptdf  6878
  Copyright terms: Public domain W3C validator