Metamath Proof Explorer

Theorem ifeqeqx

Description: An equality theorem tailored for ballotlemsf1o . (Contributed by Thierry Arnoux, 14-Apr-2017)

Ref Expression
Hypotheses ifeqeqx.1 ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐶 )
ifeqeqx.2 ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝑎 )
ifeqeqx.3 ⊢ ( 𝑥 = 𝑋 → ( 𝜒 ↔ 𝜃 ) )
ifeqeqx.4 ⊢ ( 𝑥 = 𝑌 → ( 𝜒 ↔ 𝜓 ) )
ifeqeqx.5 ⊢ ( 𝜑 → 𝑎 = 𝐶 )
ifeqeqx.6 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )
ifeqeqx.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
ifeqeqx.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
Assertion ifeqeqx ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) → 𝑎 = if ( 𝜒 , 𝐴 , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ifeqeqx.1 ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐶 )
2 ifeqeqx.2 ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝑎 )
3 ifeqeqx.3 ⊢ ( 𝑥 = 𝑋 → ( 𝜒 ↔ 𝜃 ) )
4 ifeqeqx.4 ⊢ ( 𝑥 = 𝑌 → ( 𝜒 ↔ 𝜓 ) )
5 ifeqeqx.5 ⊢ ( 𝜑 → 𝑎 = 𝐶 )
6 ifeqeqx.6 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )
7 ifeqeqx.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8 ifeqeqx.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
9 eqeq2 ⊢ ( 𝐴 = if ( 𝜒 , 𝐴 , 𝐵 ) → ( 𝑎 = 𝐴 ↔ 𝑎 = if ( 𝜒 , 𝐴 , 𝐵 ) ) )
10 eqeq2 ⊢ ( 𝐵 = if ( 𝜒 , 𝐴 , 𝐵 ) → ( 𝑎 = 𝐵 ↔ 𝑎 = if ( 𝜒 , 𝐴 , 𝐵 ) ) )
11 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ 𝜒 ) → 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) )
12 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ 𝜒 ) → 𝜑 )
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ 𝜒 ) → 𝜒 )
14 sbceq1a ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝜒 ↔ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 ) )
15 14 biimpd ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝜒 → [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 ) )
16 11 13 15 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ 𝜒 ) → [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 )
17 dfsbcq ⊢ ( 𝑋 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( [ 𝑋 / 𝑥 ] 𝜒 ↔ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 ) )
18 csbeq1 ⊢ ( 𝑋 = if ( 𝜓 , 𝑋 , 𝑌 ) → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 )
19 18 eqeq2d ⊢ ( 𝑋 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝑎 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ↔ 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 ) )
20 17 19 imbi12d ⊢ ( 𝑋 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( ( [ 𝑋 / 𝑥 ] 𝜒 → 𝑎 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ↔ ( [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 → 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 ) ) )
21 dfsbcq ⊢ ( 𝑌 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( [ 𝑌 / 𝑥 ] 𝜒 ↔ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 ) )
22 csbeq1 ⊢ ( 𝑌 = if ( 𝜓 , 𝑋 , 𝑌 ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 )
23 22 eqeq2d ⊢ ( 𝑌 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ↔ 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 ) )
24 21 23 imbi12d ⊢ ( 𝑌 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( ( [ 𝑌 / 𝑥 ] 𝜒 → 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ↔ ( [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 → 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 ) ) )
25 nfcvd ⊢ ( 𝑋 ∈ 𝑊 → Ⅎ 𝑥 𝐶 )
26 25 1 csbiegf ⊢ ( 𝑋 ∈ 𝑊 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 = 𝐶 )
27 8 26 syl ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 = 𝐶 )
28 27 5 eqtr4d ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 = 𝑎 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 = 𝑎 )
30 29 eqcomd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑎 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
31 30 a1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( [ 𝑋 / 𝑥 ] 𝜒 → 𝑎 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
32 pm3.24 ⊢ ¬ ( 𝜓 ∧ ¬ 𝜓 )
33 4 sbcieg ⊢ ( 𝑌 ∈ 𝑉 → ( [ 𝑌 / 𝑥 ] 𝜒 ↔ 𝜓 ) )
34 7 33 syl ⊢ ( 𝜑 → ( [ 𝑌 / 𝑥 ] 𝜒 ↔ 𝜓 ) )
35 34 anbi1d ⊢ ( 𝜑 → ( ( [ 𝑌 / 𝑥 ] 𝜒 ∧ ¬ 𝜓 ) ↔ ( 𝜓 ∧ ¬ 𝜓 ) ) )
36 32 35 mtbiri ⊢ ( 𝜑 → ¬ ( [ 𝑌 / 𝑥 ] 𝜒 ∧ ¬ 𝜓 ) )
37 36 pm2.21d ⊢ ( 𝜑 → ( ( [ 𝑌 / 𝑥 ] 𝜒 ∧ ¬ 𝜓 ) → 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
38 37 imp ⊢ ( ( 𝜑 ∧ ( [ 𝑌 / 𝑥 ] 𝜒 ∧ ¬ 𝜓 ) ) → 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
39 38 anass1rs ⊢ ( ( ( 𝜑 ∧ ¬ 𝜓 ) ∧ [ 𝑌 / 𝑥 ] 𝜒 ) → 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
40 39 ex ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ( [ 𝑌 / 𝑥 ] 𝜒 → 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
41 20 24 31 40 ifbothda ⊢ ( 𝜑 → ( [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 → 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 ) )
42 12 16 41 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ 𝜒 ) → 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 )
43 csbeq1a ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → 𝐴 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 )
44 43 eqeq2d ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝑎 = 𝐴 ↔ 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 ) )
45 44 biimprd ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐴 → 𝑎 = 𝐴 ) )
46 11 42 45 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ 𝜒 ) → 𝑎 = 𝐴 )
47 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ ¬ 𝜒 ) → 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) )
48 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ ¬ 𝜒 ) → 𝜑 )
49 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ ¬ 𝜒 ) → ¬ 𝜒 )
50 14 notbid ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( ¬ 𝜒 ↔ ¬ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 ) )
51 50 biimpd ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( ¬ 𝜒 → ¬ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 ) )
52 47 49 51 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ ¬ 𝜒 ) → ¬ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 )
53 17 notbid ⊢ ( 𝑋 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( ¬ [ 𝑋 / 𝑥 ] 𝜒 ↔ ¬ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 ) )
54 csbeq1 ⊢ ( 𝑋 = if ( 𝜓 , 𝑋 , 𝑌 ) → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 )
55 54 eqeq2d ⊢ ( 𝑋 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝑎 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ↔ 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 ) )
56 53 55 imbi12d ⊢ ( 𝑋 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( ( ¬ [ 𝑋 / 𝑥 ] 𝜒 → 𝑎 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ↔ ( ¬ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 → 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 ) ) )
57 21 notbid ⊢ ( 𝑌 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( ¬ [ 𝑌 / 𝑥 ] 𝜒 ↔ ¬ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 ) )
58 csbeq1 ⊢ ( 𝑌 = if ( 𝜓 , 𝑋 , 𝑌 ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 )
59 58 eqeq2d ⊢ ( 𝑌 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ↔ 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 ) )
60 57 59 imbi12d ⊢ ( 𝑌 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( ( ¬ [ 𝑌 / 𝑥 ] 𝜒 → 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ↔ ( ¬ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 → 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 ) ) )
61 3 sbcieg ⊢ ( 𝑋 ∈ 𝑊 → ( [ 𝑋 / 𝑥 ] 𝜒 ↔ 𝜃 ) )
62 8 61 syl ⊢ ( 𝜑 → ( [ 𝑋 / 𝑥 ] 𝜒 ↔ 𝜃 ) )
63 62 notbid ⊢ ( 𝜑 → ( ¬ [ 𝑋 / 𝑥 ] 𝜒 ↔ ¬ 𝜃 ) )
64 63 biimpd ⊢ ( 𝜑 → ( ¬ [ 𝑋 / 𝑥 ] 𝜒 → ¬ 𝜃 ) )
65 6 ex ⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )
66 64 65 nsyld ⊢ ( 𝜑 → ( ¬ [ 𝑋 / 𝑥 ] 𝜒 → ¬ 𝜓 ) )
67 66 anim2d ⊢ ( 𝜑 → ( ( 𝜓 ∧ ¬ [ 𝑋 / 𝑥 ] 𝜒 ) → ( 𝜓 ∧ ¬ 𝜓 ) ) )
68 32 67 mtoi ⊢ ( 𝜑 → ¬ ( 𝜓 ∧ ¬ [ 𝑋 / 𝑥 ] 𝜒 ) )
69 68 pm2.21d ⊢ ( 𝜑 → ( ( 𝜓 ∧ ¬ [ 𝑋 / 𝑥 ] 𝜒 ) → 𝑎 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
70 69 expdimp ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ¬ [ 𝑋 / 𝑥 ] 𝜒 → 𝑎 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
71 nfcvd ⊢ ( 𝑌 ∈ 𝑉 → Ⅎ 𝑥 𝑎 )
72 71 2 csbiegf ⊢ ( 𝑌 ∈ 𝑉 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 = 𝑎 )
73 7 72 syl ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 = 𝑎 )
74 73 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 = 𝑎 )
75 74 eqcomd ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
76 75 a1d ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ( ¬ [ 𝑌 / 𝑥 ] 𝜒 → 𝑎 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
77 56 60 70 76 ifbothda ⊢ ( 𝜑 → ( ¬ [ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ] 𝜒 → 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 ) )
78 48 52 77 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ ¬ 𝜒 ) → 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 )
79 csbeq1a ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → 𝐵 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 )
80 79 eqeq2d ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝑎 = 𝐵 ↔ 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 ) )
81 80 biimprd ⊢ ( 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) → ( 𝑎 = ⦋ if ( 𝜓 , 𝑋 , 𝑌 ) / 𝑥 ⦌ 𝐵 → 𝑎 = 𝐵 ) )
82 47 78 81 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) ∧ ¬ 𝜒 ) → 𝑎 = 𝐵 )
83 9 10 46 82 ifbothda ⊢ ( ( 𝜑 ∧ 𝑥 = if ( 𝜓 , 𝑋 , 𝑌 ) ) → 𝑎 = if ( 𝜒 , 𝐴 , 𝐵 ) )