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

Theorem 2nreu 4395
Description: If there are two different sets fulfilling a wff (by implicit substitution), then there is no unique set fulfilling the wff. (Contributed by AV, 20-Jun-2023.)
Hypotheses
Ref Expression
2nreu.a (𝑥 = 𝐴 → (𝜑𝜓))
2nreu.b (𝑥 = 𝐵 → (𝜑𝜒))
Assertion
Ref Expression
2nreu ((𝐴𝑋𝐵𝑋𝐴𝐵) → ((𝜓𝜒) → ¬ ∃!𝑥𝑋 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝑋   𝜒,𝑥   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 2nreu
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 simpl1 1185 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝐴𝑋)
2 simpl2 1186 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝐵𝑋)
3 simprl 767 . . . . . . 7 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝜓)
4 2nreu.b . . . . . . . . . . . 12 (𝑥 = 𝐵 → (𝜑𝜒))
54sbcieg 3813 . . . . . . . . . . 11 (𝐵𝑋 → ([𝐵 / 𝑥]𝜑𝜒))
653ad2ant2 1128 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑋𝐴𝐵) → ([𝐵 / 𝑥]𝜑𝜒))
76biimprd 249 . . . . . . . . 9 ((𝐴𝑋𝐵𝑋𝐴𝐵) → (𝜒[𝐵 / 𝑥]𝜑))
87adantld 491 . . . . . . . 8 ((𝐴𝑋𝐵𝑋𝐴𝐵) → ((𝜓𝜒) → [𝐵 / 𝑥]𝜑))
98imp 407 . . . . . . 7 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → [𝐵 / 𝑥]𝜑)
103, 9jca 512 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → (𝜓[𝐵 / 𝑥]𝜑))
11 simpl3 1187 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝐴𝐵)
12 simp1 1130 . . . . . . 7 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → 𝐴𝑋)
13 simp2 1131 . . . . . . . . 9 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → 𝐵𝑋)
14 simp3 1132 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵))
15 sbcan 3824 . . . . . . . . . . . . . 14 ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥𝑦))
16 sbcan 3824 . . . . . . . . . . . . . . . 16 ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥][𝑦 / 𝑥]𝜑))
17 2nreu.a . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐴 → (𝜑𝜓))
1817sbcieg 3813 . . . . . . . . . . . . . . . . 17 (𝐴𝑋 → ([𝐴 / 𝑥]𝜑𝜓))
19 nfs1v 2265 . . . . . . . . . . . . . . . . . 18 𝑥[𝑦 / 𝑥]𝜑
2019sbcgf 3848 . . . . . . . . . . . . . . . . 17 (𝐴𝑋 → ([𝐴 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
2118, 20anbi12d 630 . . . . . . . . . . . . . . . 16 (𝐴𝑋 → (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
2216, 21syl5bb 284 . . . . . . . . . . . . . . 15 (𝐴𝑋 → ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
23 sbcne12 4367 . . . . . . . . . . . . . . . 16 ([𝐴 / 𝑥]𝑥𝑦𝐴 / 𝑥𝑥𝐴 / 𝑥𝑦)
24 csbvarg 4386 . . . . . . . . . . . . . . . . 17 (𝐴𝑋𝐴 / 𝑥𝑥 = 𝐴)
25 csbconstg 3905 . . . . . . . . . . . . . . . . 17 (𝐴𝑋𝐴 / 𝑥𝑦 = 𝑦)
2624, 25neeq12d 3081 . . . . . . . . . . . . . . . 16 (𝐴𝑋 → (𝐴 / 𝑥𝑥𝐴 / 𝑥𝑦𝐴𝑦))
2723, 26syl5bb 284 . . . . . . . . . . . . . . 15 (𝐴𝑋 → ([𝐴 / 𝑥]𝑥𝑦𝐴𝑦))
2822, 27anbi12d 630 . . . . . . . . . . . . . 14 (𝐴𝑋 → (([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
2915, 28syl5bb 284 . . . . . . . . . . . . 13 (𝐴𝑋 → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
30293ad2ant1 1127 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
3130sbcbidv 3830 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ [𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
32 sbcan 3824 . . . . . . . . . . . 12 ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦) ↔ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴𝑦))
33 sbcan 3824 . . . . . . . . . . . . . 14 ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐵 / 𝑦]𝜓[𝐵 / 𝑦][𝑦 / 𝑥]𝜑))
34 sbcg 3850 . . . . . . . . . . . . . . . 16 (𝐵𝑋 → ([𝐵 / 𝑦]𝜓𝜓))
35 sbsbc 3779 . . . . . . . . . . . . . . . . . 18 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
3635sbcbii 3832 . . . . . . . . . . . . . . . . 17 ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑦][𝑦 / 𝑥]𝜑)
37 sbccow 3798 . . . . . . . . . . . . . . . . . 18 ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑥]𝜑)
3837a1i 11 . . . . . . . . . . . . . . . . 17 (𝐵𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
3936, 38syl5bb 284 . . . . . . . . . . . . . . . 16 (𝐵𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
4034, 39anbi12d 630 . . . . . . . . . . . . . . 15 (𝐵𝑋 → (([𝐵 / 𝑦]𝜓[𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓[𝐵 / 𝑥]𝜑)))
41403ad2ant2 1128 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → (([𝐵 / 𝑦]𝜓[𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓[𝐵 / 𝑥]𝜑)))
4233, 41syl5bb 284 . . . . . . . . . . . . 13 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓[𝐵 / 𝑥]𝜑)))
43 sbcne12 4367 . . . . . . . . . . . . . 14 ([𝐵 / 𝑦]𝐴𝑦𝐵 / 𝑦𝐴𝐵 / 𝑦𝑦)
44 csbconstg 3905 . . . . . . . . . . . . . . . 16 (𝐵𝑋𝐵 / 𝑦𝐴 = 𝐴)
45 csbvarg 4386 . . . . . . . . . . . . . . . 16 (𝐵𝑋𝐵 / 𝑦𝑦 = 𝐵)
4644, 45neeq12d 3081 . . . . . . . . . . . . . . 15 (𝐵𝑋 → (𝐵 / 𝑦𝐴𝐵 / 𝑦𝑦𝐴𝐵))
47463ad2ant2 1128 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → (𝐵 / 𝑦𝐴𝐵 / 𝑦𝑦𝐴𝐵))
4843, 47syl5bb 284 . . . . . . . . . . . . 13 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦]𝐴𝑦𝐴𝐵))
4942, 48anbi12d 630 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → (([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴𝑦) ↔ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)))
5032, 49syl5bb 284 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦) ↔ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)))
5131, 50bitrd 280 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)))
5214, 51mpbird 258 . . . . . . . . 9 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
53 rspesbca 3867 . . . . . . . . 9 ((𝐵𝑋[𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦)) → ∃𝑦𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
5413, 52, 53syl2anc 584 . . . . . . . 8 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ∃𝑦𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
55 sbcrex 3861 . . . . . . . 8 ([𝐴 / 𝑥]𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ∃𝑦𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
5654, 55sylibr 235 . . . . . . 7 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → [𝐴 / 𝑥]𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
57 rspesbca 3867 . . . . . . 7 ((𝐴𝑋[𝐴 / 𝑥]𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦)) → ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
5812, 56, 57syl2anc 584 . . . . . 6 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
591, 2, 10, 11, 58syl112anc 1368 . . . . 5 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
60 pm4.61 405 . . . . . . 7 (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦))
61 df-ne 3021 . . . . . . . . 9 (𝑥𝑦 ↔ ¬ 𝑥 = 𝑦)
6261bicomi 225 . . . . . . . 8 𝑥 = 𝑦𝑥𝑦)
6362anbi2i 622 . . . . . . 7 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
6460, 63bitri 276 . . . . . 6 (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
65642rexbii 3252 . . . . 5 (∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
6659, 65sylibr 235 . . . 4 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
6766olcd 872 . . 3 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
68 ianor 977 . . . . 5 (¬ (∃𝑥𝑋 𝜑 ∧ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
69 rexnal2 3262 . . . . . . 7 (∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
7069bicomi 225 . . . . . 6 (¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
7170orbi2i 908 . . . . 5 ((¬ ∃𝑥𝑋 𝜑 ∨ ¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
7268, 71bitri 276 . . . 4 (¬ (∃𝑥𝑋 𝜑 ∧ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
73 reu2 3719 . . . 4 (∃!𝑥𝑋 𝜑 ↔ (∃𝑥𝑋 𝜑 ∧ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
7472, 73xchnxbir 334 . . 3 (¬ ∃!𝑥𝑋 𝜑 ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
7567, 74sylibr 235 . 2 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → ¬ ∃!𝑥𝑋 𝜑)
7675ex 413 1 ((𝐴𝑋𝐵𝑋𝐴𝐵) → ((𝜓𝜒) → ¬ ∃!𝑥𝑋 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 843  w3a 1081   = wceq 1530  [wsb 2062  wcel 2106  wne 3020  wral 3142  wrex 3143  ∃!wreu 3144  [wsbc 3775  csb 3886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-nul 4295
This theorem is referenced by:  reusq0  14815  addsqn2reu  25931  addsqrexnreu  25932  addsqnreup  25933  addsq2nreurex  25934
  Copyright terms: Public domain W3C validator