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

Theorem csbie2df 4364
Description: Conversion of implicit substitution to explicit class substitution. This version of csbiedf 3886 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. Deduction form of csbie2 3895. (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 2821 . . 3 (𝜑𝐷 = 𝐷)
3 dfsbcq 3750 . . . . . 6 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝐵 = 𝐷[𝐴 / 𝑥]𝐵 = 𝐷))
4 sbceqg 4333 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐷))
54adantr 483 . . . . . . . 8 ((𝐴𝑉𝜑) → ([𝐴 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐷))
6 csbie2df.d . . . . . . . . . 10 (𝜑𝑥𝐷)
7 csbtt 3873 . . . . . . . . . 10 ((𝐴𝑉𝑥𝐷) → 𝐴 / 𝑥𝐷 = 𝐷)
86, 7sylan2 594 . . . . . . . . 9 ((𝐴𝑉𝜑) → 𝐴 / 𝑥𝐷 = 𝐷)
98eqeq2d 2831 . . . . . . . 8 ((𝐴𝑉𝜑) → (𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐷𝐴 / 𝑥𝐵 = 𝐷))
105, 9bitrd 281 . . . . . . 7 ((𝐴𝑉𝜑) → ([𝐴 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐷))
111, 10mpancom 686 . . . . . 6 (𝜑 → ([𝐴 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐷))
123, 11sylan9bb 512 . . . . 5 ((𝑦 = 𝐴𝜑) → ([𝑦 / 𝑥]𝐵 = 𝐷𝐴 / 𝑥𝐵 = 𝐷))
1312pm5.74da 802 . . . 4 (𝑦 = 𝐴 → ((𝜑[𝑦 / 𝑥]𝐵 = 𝐷) ↔ (𝜑𝐴 / 𝑥𝐵 = 𝐷)))
14 csbie2df.2 . . . . . . 7 ((𝜑𝑦 = 𝐴) → 𝐶 = 𝐷)
1514eqeq1d 2822 . . . . . 6 ((𝜑𝑦 = 𝐴) → (𝐶 = 𝐷𝐷 = 𝐷))
1615expcom 416 . . . . 5 (𝑦 = 𝐴 → (𝜑 → (𝐶 = 𝐷𝐷 = 𝐷)))
1716pm5.74d 275 . . . 4 (𝑦 = 𝐴 → ((𝜑𝐶 = 𝐷) ↔ (𝜑𝐷 = 𝐷)))
18 sbsbc 3752 . . . . . 6 ([𝑦 / 𝑥]𝐵 = 𝐷[𝑦 / 𝑥]𝐵 = 𝐷)
19 csbie2df.p . . . . . . 7 𝑥𝜑
20 csbie2df.c . . . . . . . 8 (𝜑𝑥𝐶)
2120, 6nfeqd 2983 . . . . . . 7 (𝜑 → Ⅎ𝑥 𝐶 = 𝐷)
22 csbie2df.1 . . . . . . . . 9 ((𝜑𝑥 = 𝑦) → 𝐵 = 𝐶)
2322eqeq1d 2822 . . . . . . . 8 ((𝜑𝑥 = 𝑦) → (𝐵 = 𝐷𝐶 = 𝐷))
2423ex 415 . . . . . . 7 (𝜑 → (𝑥 = 𝑦 → (𝐵 = 𝐷𝐶 = 𝐷)))
2519, 21, 24sbiedw 2332 . . . . . 6 (𝜑 → ([𝑦 / 𝑥]𝐵 = 𝐷𝐶 = 𝐷))
2618, 25syl5bbr 287 . . . . 5 (𝜑 → ([𝑦 / 𝑥]𝐵 = 𝐷𝐶 = 𝐷))
2726pm5.74i 273 . . . 4 ((𝜑[𝑦 / 𝑥]𝐵 = 𝐷) ↔ (𝜑𝐶 = 𝐷))
2813, 17, 27vtoclbg 3545 . . 3 (𝐴𝑉 → ((𝜑𝐴 / 𝑥𝐵 = 𝐷) ↔ (𝜑𝐷 = 𝐷)))
292, 28mpbiri 260 . 2 (𝐴𝑉 → (𝜑𝐴 / 𝑥𝐵 = 𝐷))
301, 29mpcom 38 1 (𝜑𝐴 / 𝑥𝐵 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1537  wnf 1784  [wsb 2069  wcel 2114  wnfc 2957  [wsbc 3748  csb 3856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-sbc 3749  df-csb 3857
This theorem is referenced by:  fvmptdf  6746
  Copyright terms: Public domain W3C validator