Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifeqeqx Structured version   Visualization version   GIF version

Theorem ifeqeqx 29487
Description: An equality theorem tailored for ballotlemsf1o 30703. (Contributed by Thierry Arnoux, 14-Apr-2017.)
Hypotheses
Ref Expression
ifeqeqx.1 (𝑥 = 𝑋𝐴 = 𝐶)
ifeqeqx.2 (𝑥 = 𝑌𝐵 = 𝑎)
ifeqeqx.3 (𝑥 = 𝑋 → (𝜒𝜃))
ifeqeqx.4 (𝑥 = 𝑌 → (𝜒𝜓))
ifeqeqx.5 (𝜑𝑎 = 𝐶)
ifeqeqx.6 ((𝜑𝜓) → 𝜃)
ifeqeqx.y (𝜑𝑌𝑉)
ifeqeqx.x (𝜑𝑋𝑊)
Assertion
Ref Expression
ifeqeqx ((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))
Distinct variable groups:   𝑥,𝑎   𝑥,𝐶   𝑥,𝑋   𝑥,𝑌   𝑥,𝑉   𝑥,𝑊   𝜓,𝑥   𝜃,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑎)   𝜓(𝑎)   𝜒(𝑥,𝑎)   𝜃(𝑎)   𝐴(𝑥,𝑎)   𝐵(𝑥,𝑎)   𝐶(𝑎)   𝑉(𝑎)   𝑊(𝑎)   𝑋(𝑎)   𝑌(𝑎)

Proof of Theorem ifeqeqx
StepHypRef Expression
1 eqeq2 2662 . 2 (𝐴 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐴𝑎 = if(𝜒, 𝐴, 𝐵)))
2 eqeq2 2662 . 2 (𝐵 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐵𝑎 = if(𝜒, 𝐴, 𝐵)))
3 simplr 807 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
4 simpll 805 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜑)
5 simpr 476 . . . . 5 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜒)
6 sbceq1a 3479 . . . . . 6 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
76biimpd 219 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
83, 5, 7sylc 65 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
9 dfsbcq 3470 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → ([𝑋 / 𝑥]𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
10 csbeq1 3569 . . . . . . 7 (𝑋 = if(𝜓, 𝑋, 𝑌) → 𝑋 / 𝑥𝐴 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
1110eqeq2d 2661 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑋 / 𝑥𝐴𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
129, 11imbi12d 333 . . . . 5 (𝑋 = if(𝜓, 𝑋, 𝑌) → (([𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)))
13 dfsbcq 3470 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → ([𝑌 / 𝑥]𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
14 csbeq1 3569 . . . . . . 7 (𝑌 = if(𝜓, 𝑋, 𝑌) → 𝑌 / 𝑥𝐴 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
1514eqeq2d 2661 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑌 / 𝑥𝐴𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
1613, 15imbi12d 333 . . . . 5 (𝑌 = if(𝜓, 𝑋, 𝑌) → (([𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)))
17 ifeqeqx.x . . . . . . . . . 10 (𝜑𝑋𝑊)
18 nfcvd 2794 . . . . . . . . . . 11 (𝑋𝑊𝑥𝐶)
19 ifeqeqx.1 . . . . . . . . . . 11 (𝑥 = 𝑋𝐴 = 𝐶)
2018, 19csbiegf 3590 . . . . . . . . . 10 (𝑋𝑊𝑋 / 𝑥𝐴 = 𝐶)
2117, 20syl 17 . . . . . . . . 9 (𝜑𝑋 / 𝑥𝐴 = 𝐶)
22 ifeqeqx.5 . . . . . . . . 9 (𝜑𝑎 = 𝐶)
2321, 22eqtr4d 2688 . . . . . . . 8 (𝜑𝑋 / 𝑥𝐴 = 𝑎)
2423adantr 480 . . . . . . 7 ((𝜑𝜓) → 𝑋 / 𝑥𝐴 = 𝑎)
2524eqcomd 2657 . . . . . 6 ((𝜑𝜓) → 𝑎 = 𝑋 / 𝑥𝐴)
2625a1d 25 . . . . 5 ((𝜑𝜓) → ([𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐴))
27 pm3.24 944 . . . . . . . . . 10 ¬ (𝜓 ∧ ¬ 𝜓)
28 ifeqeqx.y . . . . . . . . . . . 12 (𝜑𝑌𝑉)
29 ifeqeqx.4 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → (𝜒𝜓))
3029sbcieg 3501 . . . . . . . . . . . 12 (𝑌𝑉 → ([𝑌 / 𝑥]𝜒𝜓))
3128, 30syl 17 . . . . . . . . . . 11 (𝜑 → ([𝑌 / 𝑥]𝜒𝜓))
3231anbi1d 741 . . . . . . . . . 10 (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) ↔ (𝜓 ∧ ¬ 𝜓)))
3327, 32mtbiri 316 . . . . . . . . 9 (𝜑 → ¬ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓))
3433pm2.21d 118 . . . . . . . 8 (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) → 𝑎 = 𝑌 / 𝑥𝐴))
3534imp 444 . . . . . . 7 ((𝜑 ∧ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓)) → 𝑎 = 𝑌 / 𝑥𝐴)
3635anass1rs 866 . . . . . 6 (((𝜑 ∧ ¬ 𝜓) ∧ [𝑌 / 𝑥]𝜒) → 𝑎 = 𝑌 / 𝑥𝐴)
3736ex 449 . . . . 5 ((𝜑 ∧ ¬ 𝜓) → ([𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐴))
3812, 16, 26, 37ifbothda 4156 . . . 4 (𝜑 → ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
394, 8, 38sylc 65 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
40 csbeq1a 3575 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐴 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
4140eqeq2d 2661 . . . 4 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐴𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
4241biimprd 238 . . 3 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴𝑎 = 𝐴))
433, 39, 42sylc 65 . 2 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = 𝐴)
44 simplr 807 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
45 simpll 805 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝜑)
46 simpr 476 . . . . 5 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ 𝜒)
476notbid 307 . . . . . 6 (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
4847biimpd 219 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
4944, 46, 48sylc 65 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
509notbid 307 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
51 csbeq1 3569 . . . . . . 7 (𝑋 = if(𝜓, 𝑋, 𝑌) → 𝑋 / 𝑥𝐵 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
5251eqeq2d 2661 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑋 / 𝑥𝐵𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
5350, 52imbi12d 333 . . . . 5 (𝑋 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)))
5413notbid 307 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑌 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
55 csbeq1 3569 . . . . . . 7 (𝑌 = if(𝜓, 𝑋, 𝑌) → 𝑌 / 𝑥𝐵 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
5655eqeq2d 2661 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑌 / 𝑥𝐵𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
5754, 56imbi12d 333 . . . . 5 (𝑌 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)))
58 ifeqeqx.3 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝜒𝜃))
5958sbcieg 3501 . . . . . . . . . . . . 13 (𝑋𝑊 → ([𝑋 / 𝑥]𝜒𝜃))
6017, 59syl 17 . . . . . . . . . . . 12 (𝜑 → ([𝑋 / 𝑥]𝜒𝜃))
6160notbid 307 . . . . . . . . . . 11 (𝜑 → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ 𝜃))
6261biimpd 219 . . . . . . . . . 10 (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜃))
63 ifeqeqx.6 . . . . . . . . . . 11 ((𝜑𝜓) → 𝜃)
6463ex 449 . . . . . . . . . 10 (𝜑 → (𝜓𝜃))
6562, 64nsyld 154 . . . . . . . . 9 (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜓))
6665anim2d 588 . . . . . . . 8 (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → (𝜓 ∧ ¬ 𝜓)))
6727, 66mtoi 190 . . . . . . 7 (𝜑 → ¬ (𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒))
6867pm2.21d 118 . . . . . 6 (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → 𝑎 = 𝑋 / 𝑥𝐵))
6968expdimp 452 . . . . 5 ((𝜑𝜓) → (¬ [𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐵))
70 nfcvd 2794 . . . . . . . . . 10 (𝑌𝑉𝑥𝑎)
71 ifeqeqx.2 . . . . . . . . . 10 (𝑥 = 𝑌𝐵 = 𝑎)
7270, 71csbiegf 3590 . . . . . . . . 9 (𝑌𝑉𝑌 / 𝑥𝐵 = 𝑎)
7328, 72syl 17 . . . . . . . 8 (𝜑𝑌 / 𝑥𝐵 = 𝑎)
7473adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝜓) → 𝑌 / 𝑥𝐵 = 𝑎)
7574eqcomd 2657 . . . . . 6 ((𝜑 ∧ ¬ 𝜓) → 𝑎 = 𝑌 / 𝑥𝐵)
7675a1d 25 . . . . 5 ((𝜑 ∧ ¬ 𝜓) → (¬ [𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐵))
7753, 57, 69, 76ifbothda 4156 . . . 4 (𝜑 → (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
7845, 49, 77sylc 65 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
79 csbeq1a 3575 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐵 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
8079eqeq2d 2661 . . . 4 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐵𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
8180biimprd 238 . . 3 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵𝑎 = 𝐵))
8244, 78, 81sylc 65 . 2 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = 𝐵)
831, 2, 43, 82ifbothda 4156 1 ((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  [wsbc 3468  csb 3566  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sbc 3469  df-csb 3567  df-if 4120
This theorem is referenced by:  ballotlemsf1o  30703
  Copyright terms: Public domain W3C validator