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 28563
Description: An equality theorem tailored for ballotlemsf1o 29739. (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 2525 . 2 (𝐴 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐴𝑎 = if(𝜒, 𝐴, 𝐵)))
2 eqeq2 2525 . 2 (𝐵 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐵𝑎 = if(𝜒, 𝐴, 𝐵)))
3 simplr 787 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
4 simpll 785 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜑)
5 simpr 475 . . . . 5 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜒)
6 sbceq1a 3317 . . . . . 6 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
76biimpd 217 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
83, 5, 7sylc 62 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
9 dfsbcq 3308 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → ([𝑋 / 𝑥]𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
10 csbeq1 3406 . . . . . . 7 (𝑋 = if(𝜓, 𝑋, 𝑌) → 𝑋 / 𝑥𝐴 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
1110eqeq2d 2524 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑋 / 𝑥𝐴𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
129, 11imbi12d 332 . . . . 5 (𝑋 = if(𝜓, 𝑋, 𝑌) → (([𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)))
13 dfsbcq 3308 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → ([𝑌 / 𝑥]𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
14 csbeq1 3406 . . . . . . 7 (𝑌 = if(𝜓, 𝑋, 𝑌) → 𝑌 / 𝑥𝐴 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
1514eqeq2d 2524 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑌 / 𝑥𝐴𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
1613, 15imbi12d 332 . . . . 5 (𝑌 = if(𝜓, 𝑋, 𝑌) → (([𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)))
17 ifeqeqx.x . . . . . . . . . 10 (𝜑𝑋𝑊)
18 nfcvd 2656 . . . . . . . . . . 11 (𝑋𝑊𝑥𝐶)
19 ifeqeqx.1 . . . . . . . . . . 11 (𝑥 = 𝑋𝐴 = 𝐶)
2018, 19csbiegf 3427 . . . . . . . . . 10 (𝑋𝑊𝑋 / 𝑥𝐴 = 𝐶)
2117, 20syl 17 . . . . . . . . 9 (𝜑𝑋 / 𝑥𝐴 = 𝐶)
22 ifeqeqx.5 . . . . . . . . 9 (𝜑𝑎 = 𝐶)
2321, 22eqtr4d 2551 . . . . . . . 8 (𝜑𝑋 / 𝑥𝐴 = 𝑎)
2423adantr 479 . . . . . . 7 ((𝜑𝜓) → 𝑋 / 𝑥𝐴 = 𝑎)
2524eqcomd 2520 . . . . . 6 ((𝜑𝜓) → 𝑎 = 𝑋 / 𝑥𝐴)
2625a1d 25 . . . . 5 ((𝜑𝜓) → ([𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐴))
27 pm3.24 921 . . . . . . . . . 10 ¬ (𝜓 ∧ ¬ 𝜓)
28 ifeqeqx.y . . . . . . . . . . . 12 (𝜑𝑌𝑉)
29 ifeqeqx.4 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → (𝜒𝜓))
3029sbcieg 3339 . . . . . . . . . . . 12 (𝑌𝑉 → ([𝑌 / 𝑥]𝜒𝜓))
3128, 30syl 17 . . . . . . . . . . 11 (𝜑 → ([𝑌 / 𝑥]𝜒𝜓))
3231anbi1d 736 . . . . . . . . . 10 (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) ↔ (𝜓 ∧ ¬ 𝜓)))
3327, 32mtbiri 315 . . . . . . . . 9 (𝜑 → ¬ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓))
3433pm2.21d 116 . . . . . . . 8 (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) → 𝑎 = 𝑌 / 𝑥𝐴))
3534imp 443 . . . . . . 7 ((𝜑 ∧ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓)) → 𝑎 = 𝑌 / 𝑥𝐴)
3635anass1rs 844 . . . . . 6 (((𝜑 ∧ ¬ 𝜓) ∧ [𝑌 / 𝑥]𝜒) → 𝑎 = 𝑌 / 𝑥𝐴)
3736ex 448 . . . . 5 ((𝜑 ∧ ¬ 𝜓) → ([𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐴))
3812, 16, 26, 37ifbothda 3976 . . . 4 (𝜑 → ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
394, 8, 38sylc 62 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
40 csbeq1a 3412 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐴 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
4140eqeq2d 2524 . . . 4 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐴𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
4241biimprd 236 . . 3 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴𝑎 = 𝐴))
433, 39, 42sylc 62 . 2 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = 𝐴)
44 simplr 787 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
45 simpll 785 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝜑)
46 simpr 475 . . . . 5 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ 𝜒)
476notbid 306 . . . . . 6 (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
4847biimpd 217 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
4944, 46, 48sylc 62 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
509notbid 306 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
51 csbeq1 3406 . . . . . . 7 (𝑋 = if(𝜓, 𝑋, 𝑌) → 𝑋 / 𝑥𝐵 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
5251eqeq2d 2524 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑋 / 𝑥𝐵𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
5350, 52imbi12d 332 . . . . 5 (𝑋 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)))
5413notbid 306 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑌 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
55 csbeq1 3406 . . . . . . 7 (𝑌 = if(𝜓, 𝑋, 𝑌) → 𝑌 / 𝑥𝐵 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
5655eqeq2d 2524 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑌 / 𝑥𝐵𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
5754, 56imbi12d 332 . . . . 5 (𝑌 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)))
58 ifeqeqx.3 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝜒𝜃))
5958sbcieg 3339 . . . . . . . . . . . . 13 (𝑋𝑊 → ([𝑋 / 𝑥]𝜒𝜃))
6017, 59syl 17 . . . . . . . . . . . 12 (𝜑 → ([𝑋 / 𝑥]𝜒𝜃))
6160notbid 306 . . . . . . . . . . 11 (𝜑 → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ 𝜃))
6261biimpd 217 . . . . . . . . . 10 (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜃))
63 ifeqeqx.6 . . . . . . . . . . 11 ((𝜑𝜓) → 𝜃)
6463ex 448 . . . . . . . . . 10 (𝜑 → (𝜓𝜃))
6562, 64nsyld 152 . . . . . . . . 9 (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜓))
6665anim2d 586 . . . . . . . 8 (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → (𝜓 ∧ ¬ 𝜓)))
6727, 66mtoi 188 . . . . . . 7 (𝜑 → ¬ (𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒))
6867pm2.21d 116 . . . . . 6 (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → 𝑎 = 𝑋 / 𝑥𝐵))
6968expdimp 451 . . . . 5 ((𝜑𝜓) → (¬ [𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐵))
70 nfcvd 2656 . . . . . . . . . 10 (𝑌𝑉𝑥𝑎)
71 ifeqeqx.2 . . . . . . . . . 10 (𝑥 = 𝑌𝐵 = 𝑎)
7270, 71csbiegf 3427 . . . . . . . . 9 (𝑌𝑉𝑌 / 𝑥𝐵 = 𝑎)
7328, 72syl 17 . . . . . . . 8 (𝜑𝑌 / 𝑥𝐵 = 𝑎)
7473adantr 479 . . . . . . 7 ((𝜑 ∧ ¬ 𝜓) → 𝑌 / 𝑥𝐵 = 𝑎)
7574eqcomd 2520 . . . . . 6 ((𝜑 ∧ ¬ 𝜓) → 𝑎 = 𝑌 / 𝑥𝐵)
7675a1d 25 . . . . 5 ((𝜑 ∧ ¬ 𝜓) → (¬ [𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐵))
7753, 57, 69, 76ifbothda 3976 . . . 4 (𝜑 → (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
7845, 49, 77sylc 62 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
79 csbeq1a 3412 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐵 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
8079eqeq2d 2524 . . . 4 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐵𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
8180biimprd 236 . . 3 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵𝑎 = 𝐵))
8244, 78, 81sylc 62 . 2 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = 𝐵)
831, 2, 43, 82ifbothda 3976 1 ((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  [wsbc 3306  csb 3403  ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079  df-sbc 3307  df-csb 3404  df-if 3940
This theorem is referenced by:  ballotlemsf1o  29739  ballotlemsf1oOLD  29777
  Copyright terms: Public domain W3C validator