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 29333
Description: An equality theorem tailored for ballotlemsf1o 30549. (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 2631 . 2 (𝐴 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐴𝑎 = if(𝜒, 𝐴, 𝐵)))
2 eqeq2 2631 . 2 (𝐵 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐵𝑎 = if(𝜒, 𝐴, 𝐵)))
3 simplr 791 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
4 simpll 789 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜑)
5 simpr 477 . . . . 5 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜒)
6 sbceq1a 3440 . . . . . 6 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
76biimpd 219 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
83, 5, 7sylc 65 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
9 dfsbcq 3431 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → ([𝑋 / 𝑥]𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
10 csbeq1 3529 . . . . . . 7 (𝑋 = if(𝜓, 𝑋, 𝑌) → 𝑋 / 𝑥𝐴 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
1110eqeq2d 2630 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑋 / 𝑥𝐴𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
129, 11imbi12d 334 . . . . 5 (𝑋 = if(𝜓, 𝑋, 𝑌) → (([𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)))
13 dfsbcq 3431 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → ([𝑌 / 𝑥]𝜒[if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
14 csbeq1 3529 . . . . . . 7 (𝑌 = if(𝜓, 𝑋, 𝑌) → 𝑌 / 𝑥𝐴 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
1514eqeq2d 2630 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑌 / 𝑥𝐴𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
1613, 15imbi12d 334 . . . . 5 (𝑌 = if(𝜓, 𝑋, 𝑌) → (([𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)))
17 ifeqeqx.x . . . . . . . . . 10 (𝜑𝑋𝑊)
18 nfcvd 2763 . . . . . . . . . . 11 (𝑋𝑊𝑥𝐶)
19 ifeqeqx.1 . . . . . . . . . . 11 (𝑥 = 𝑋𝐴 = 𝐶)
2018, 19csbiegf 3550 . . . . . . . . . 10 (𝑋𝑊𝑋 / 𝑥𝐴 = 𝐶)
2117, 20syl 17 . . . . . . . . 9 (𝜑𝑋 / 𝑥𝐴 = 𝐶)
22 ifeqeqx.5 . . . . . . . . 9 (𝜑𝑎 = 𝐶)
2321, 22eqtr4d 2657 . . . . . . . 8 (𝜑𝑋 / 𝑥𝐴 = 𝑎)
2423adantr 481 . . . . . . 7 ((𝜑𝜓) → 𝑋 / 𝑥𝐴 = 𝑎)
2524eqcomd 2626 . . . . . 6 ((𝜑𝜓) → 𝑎 = 𝑋 / 𝑥𝐴)
2625a1d 25 . . . . 5 ((𝜑𝜓) → ([𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐴))
27 pm3.24 925 . . . . . . . . . 10 ¬ (𝜓 ∧ ¬ 𝜓)
28 ifeqeqx.y . . . . . . . . . . . 12 (𝜑𝑌𝑉)
29 ifeqeqx.4 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → (𝜒𝜓))
3029sbcieg 3462 . . . . . . . . . . . 12 (𝑌𝑉 → ([𝑌 / 𝑥]𝜒𝜓))
3128, 30syl 17 . . . . . . . . . . 11 (𝜑 → ([𝑌 / 𝑥]𝜒𝜓))
3231anbi1d 740 . . . . . . . . . 10 (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) ↔ (𝜓 ∧ ¬ 𝜓)))
3327, 32mtbiri 317 . . . . . . . . 9 (𝜑 → ¬ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓))
3433pm2.21d 118 . . . . . . . 8 (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) → 𝑎 = 𝑌 / 𝑥𝐴))
3534imp 445 . . . . . . 7 ((𝜑 ∧ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓)) → 𝑎 = 𝑌 / 𝑥𝐴)
3635anass1rs 848 . . . . . 6 (((𝜑 ∧ ¬ 𝜓) ∧ [𝑌 / 𝑥]𝜒) → 𝑎 = 𝑌 / 𝑥𝐴)
3736ex 450 . . . . 5 ((𝜑 ∧ ¬ 𝜓) → ([𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐴))
3812, 16, 26, 37ifbothda 4114 . . . 4 (𝜑 → ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
394, 8, 38sylc 65 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
40 csbeq1a 3535 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐴 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴)
4140eqeq2d 2630 . . . 4 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐴𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴))
4241biimprd 238 . . 3 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐴𝑎 = 𝐴))
433, 39, 42sylc 65 . 2 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = 𝐴)
44 simplr 791 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
45 simpll 789 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝜑)
46 simpr 477 . . . . 5 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ 𝜒)
476notbid 308 . . . . . 6 (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
4847biimpd 219 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
4944, 46, 48sylc 65 . . . 4 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
509notbid 308 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
51 csbeq1 3529 . . . . . . 7 (𝑋 = if(𝜓, 𝑋, 𝑌) → 𝑋 / 𝑥𝐵 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
5251eqeq2d 2630 . . . . . 6 (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑋 / 𝑥𝐵𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
5350, 52imbi12d 334 . . . . 5 (𝑋 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)))
5413notbid 308 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑌 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
55 csbeq1 3529 . . . . . . 7 (𝑌 = if(𝜓, 𝑋, 𝑌) → 𝑌 / 𝑥𝐵 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
5655eqeq2d 2630 . . . . . 6 (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝑌 / 𝑥𝐵𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
5754, 56imbi12d 334 . . . . 5 (𝑌 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)))
58 ifeqeqx.3 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝜒𝜃))
5958sbcieg 3462 . . . . . . . . . . . . 13 (𝑋𝑊 → ([𝑋 / 𝑥]𝜒𝜃))
6017, 59syl 17 . . . . . . . . . . . 12 (𝜑 → ([𝑋 / 𝑥]𝜒𝜃))
6160notbid 308 . . . . . . . . . . 11 (𝜑 → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ 𝜃))
6261biimpd 219 . . . . . . . . . 10 (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜃))
63 ifeqeqx.6 . . . . . . . . . . 11 ((𝜑𝜓) → 𝜃)
6463ex 450 . . . . . . . . . 10 (𝜑 → (𝜓𝜃))
6562, 64nsyld 154 . . . . . . . . 9 (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜓))
6665anim2d 588 . . . . . . . 8 (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → (𝜓 ∧ ¬ 𝜓)))
6727, 66mtoi 190 . . . . . . 7 (𝜑 → ¬ (𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒))
6867pm2.21d 118 . . . . . 6 (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → 𝑎 = 𝑋 / 𝑥𝐵))
6968expdimp 453 . . . . 5 ((𝜑𝜓) → (¬ [𝑋 / 𝑥]𝜒𝑎 = 𝑋 / 𝑥𝐵))
70 nfcvd 2763 . . . . . . . . . 10 (𝑌𝑉𝑥𝑎)
71 ifeqeqx.2 . . . . . . . . . 10 (𝑥 = 𝑌𝐵 = 𝑎)
7270, 71csbiegf 3550 . . . . . . . . 9 (𝑌𝑉𝑌 / 𝑥𝐵 = 𝑎)
7328, 72syl 17 . . . . . . . 8 (𝜑𝑌 / 𝑥𝐵 = 𝑎)
7473adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ 𝜓) → 𝑌 / 𝑥𝐵 = 𝑎)
7574eqcomd 2626 . . . . . 6 ((𝜑 ∧ ¬ 𝜓) → 𝑎 = 𝑌 / 𝑥𝐵)
7675a1d 25 . . . . 5 ((𝜑 ∧ ¬ 𝜓) → (¬ [𝑌 / 𝑥]𝜒𝑎 = 𝑌 / 𝑥𝐵))
7753, 57, 69, 76ifbothda 4114 . . . 4 (𝜑 → (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
7845, 49, 77sylc 65 . . 3 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
79 csbeq1a 3535 . . . . 5 (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐵 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵)
8079eqeq2d 2630 . . . 4 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐵𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵))
8180biimprd 238 . . 3 (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = if(𝜓, 𝑋, 𝑌) / 𝑥𝐵𝑎 = 𝐵))
8244, 78, 81sylc 65 . 2 (((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = 𝐵)
831, 2, 43, 82ifbothda 4114 1 ((𝜑𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  [wsbc 3429  csb 3526  ifcif 4077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-sbc 3430  df-csb 3527  df-if 4078
This theorem is referenced by:  ballotlemsf1o  30549
  Copyright terms: Public domain W3C validator