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

Theorem 2nreu 4375
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 1190 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝐴𝑋)
2 simpl2 1191 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝐵𝑋)
3 simprl 768 . . . . . . 7 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝜓)
4 2nreu.b . . . . . . . . . . . 12 (𝑥 = 𝐵 → (𝜑𝜒))
54sbcieg 3756 . . . . . . . . . . 11 (𝐵𝑋 → ([𝐵 / 𝑥]𝜑𝜒))
653ad2ant2 1133 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑋𝐴𝐵) → ([𝐵 / 𝑥]𝜑𝜒))
76biimprd 247 . . . . . . . . 9 ((𝐴𝑋𝐵𝑋𝐴𝐵) → (𝜒[𝐵 / 𝑥]𝜑))
87adantld 491 . . . . . . . 8 ((𝐴𝑋𝐵𝑋𝐴𝐵) → ((𝜓𝜒) → [𝐵 / 𝑥]𝜑))
98imp 407 . . . . . . 7 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → [𝐵 / 𝑥]𝜑)
103, 9jca 512 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → (𝜓[𝐵 / 𝑥]𝜑))
11 simpl3 1192 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝐴𝐵)
12 simp1 1135 . . . . . . 7 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → 𝐴𝑋)
13 simp2 1136 . . . . . . . . 9 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → 𝐵𝑋)
14 simp3 1137 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵))
15 sbcan 3768 . . . . . . . . . . . . . 14 ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥𝑦))
16 sbcan 3768 . . . . . . . . . . . . . . . 16 ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥][𝑦 / 𝑥]𝜑))
17 2nreu.a . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐴 → (𝜑𝜓))
1817sbcieg 3756 . . . . . . . . . . . . . . . . 17 (𝐴𝑋 → ([𝐴 / 𝑥]𝜑𝜓))
19 nfs1v 2153 . . . . . . . . . . . . . . . . . 18 𝑥[𝑦 / 𝑥]𝜑
2019sbcgf 3793 . . . . . . . . . . . . . . . . 17 (𝐴𝑋 → ([𝐴 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
2118, 20anbi12d 631 . . . . . . . . . . . . . . . 16 (𝐴𝑋 → (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
2216, 21bitrid 282 . . . . . . . . . . . . . . 15 (𝐴𝑋 → ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
23 sbcne12 4346 . . . . . . . . . . . . . . . 16 ([𝐴 / 𝑥]𝑥𝑦𝐴 / 𝑥𝑥𝐴 / 𝑥𝑦)
24 csbvarg 4365 . . . . . . . . . . . . . . . . 17 (𝐴𝑋𝐴 / 𝑥𝑥 = 𝐴)
25 csbconstg 3851 . . . . . . . . . . . . . . . . 17 (𝐴𝑋𝐴 / 𝑥𝑦 = 𝑦)
2624, 25neeq12d 3005 . . . . . . . . . . . . . . . 16 (𝐴𝑋 → (𝐴 / 𝑥𝑥𝐴 / 𝑥𝑦𝐴𝑦))
2723, 26bitrid 282 . . . . . . . . . . . . . . 15 (𝐴𝑋 → ([𝐴 / 𝑥]𝑥𝑦𝐴𝑦))
2822, 27anbi12d 631 . . . . . . . . . . . . . 14 (𝐴𝑋 → (([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
2915, 28bitrid 282 . . . . . . . . . . . . 13 (𝐴𝑋 → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
30293ad2ant1 1132 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
3130sbcbidv 3775 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ [𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
32 sbcan 3768 . . . . . . . . . . . 12 ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦) ↔ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴𝑦))
33 sbcan 3768 . . . . . . . . . . . . . 14 ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐵 / 𝑦]𝜓[𝐵 / 𝑦][𝑦 / 𝑥]𝜑))
34 sbcg 3795 . . . . . . . . . . . . . . . 16 (𝐵𝑋 → ([𝐵 / 𝑦]𝜓𝜓))
35 sbsbc 3720 . . . . . . . . . . . . . . . . . 18 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
3635sbcbii 3776 . . . . . . . . . . . . . . . . 17 ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑦][𝑦 / 𝑥]𝜑)
37 sbccow 3739 . . . . . . . . . . . . . . . . . 18 ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑥]𝜑)
3837a1i 11 . . . . . . . . . . . . . . . . 17 (𝐵𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
3936, 38bitrid 282 . . . . . . . . . . . . . . . 16 (𝐵𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
4034, 39anbi12d 631 . . . . . . . . . . . . . . 15 (𝐵𝑋 → (([𝐵 / 𝑦]𝜓[𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓[𝐵 / 𝑥]𝜑)))
41403ad2ant2 1133 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → (([𝐵 / 𝑦]𝜓[𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓[𝐵 / 𝑥]𝜑)))
4233, 41bitrid 282 . . . . . . . . . . . . 13 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓[𝐵 / 𝑥]𝜑)))
43 sbcne12 4346 . . . . . . . . . . . . . 14 ([𝐵 / 𝑦]𝐴𝑦𝐵 / 𝑦𝐴𝐵 / 𝑦𝑦)
44 csbconstg 3851 . . . . . . . . . . . . . . . 16 (𝐵𝑋𝐵 / 𝑦𝐴 = 𝐴)
45 csbvarg 4365 . . . . . . . . . . . . . . . 16 (𝐵𝑋𝐵 / 𝑦𝑦 = 𝐵)
4644, 45neeq12d 3005 . . . . . . . . . . . . . . 15 (𝐵𝑋 → (𝐵 / 𝑦𝐴𝐵 / 𝑦𝑦𝐴𝐵))
47463ad2ant2 1133 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → (𝐵 / 𝑦𝐴𝐵 / 𝑦𝑦𝐴𝐵))
4843, 47bitrid 282 . . . . . . . . . . . . 13 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦]𝐴𝑦𝐴𝐵))
4942, 48anbi12d 631 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → (([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴𝑦) ↔ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)))
5032, 49bitrid 282 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦) ↔ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)))
5131, 50bitrd 278 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)))
5214, 51mpbird 256 . . . . . . . . 9 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
53 rspesbca 3814 . . . . . . . . 9 ((𝐵𝑋[𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦)) → ∃𝑦𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
5413, 52, 53syl2anc 584 . . . . . . . 8 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ∃𝑦𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
55 sbcrex 3808 . . . . . . . 8 ([𝐴 / 𝑥]𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ∃𝑦𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
5654, 55sylibr 233 . . . . . . 7 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → [𝐴 / 𝑥]𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
57 rspesbca 3814 . . . . . . 7 ((𝐴𝑋[𝐴 / 𝑥]𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦)) → ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
5812, 56, 57syl2anc 584 . . . . . 6 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
591, 2, 10, 11, 58syl112anc 1373 . . . . 5 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
60 pm4.61 405 . . . . . . 7 (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦))
61 df-ne 2944 . . . . . . . . 9 (𝑥𝑦 ↔ ¬ 𝑥 = 𝑦)
6261bicomi 223 . . . . . . . 8 𝑥 = 𝑦𝑥𝑦)
6362anbi2i 623 . . . . . . 7 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
6460, 63bitri 274 . . . . . 6 (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
65642rexbii 3182 . . . . 5 (∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
6659, 65sylibr 233 . . . 4 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
6766olcd 871 . . 3 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
68 ianor 979 . . . . 5 (¬ (∃𝑥𝑋 𝜑 ∧ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
69 rexnal2 3187 . . . . . . 7 (∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
7069bicomi 223 . . . . . 6 (¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
7170orbi2i 910 . . . . 5 ((¬ ∃𝑥𝑋 𝜑 ∨ ¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
7268, 71bitri 274 . . . 4 (¬ (∃𝑥𝑋 𝜑 ∧ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
73 reu2 3660 . . . 4 (∃!𝑥𝑋 𝜑 ↔ (∃𝑥𝑋 𝜑 ∧ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
7472, 73xchnxbir 333 . . 3 (¬ ∃!𝑥𝑋 𝜑 ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
7567, 74sylibr 233 . 2 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → ¬ ∃!𝑥𝑋 𝜑)
7675ex 413 1 ((𝐴𝑋𝐵𝑋𝐴𝐵) → ((𝜓𝜒) → ¬ ∃!𝑥𝑋 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1539  [wsb 2067  wcel 2106  wne 2943  wral 3064  wrex 3065  ∃!wreu 3066  [wsbc 3716  csb 3832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-nul 4257
This theorem is referenced by:  reusq0  15174  addsqn2reu  26589  addsqrexnreu  26590  addsqnreup  26591  addsq2nreurex  26592
  Copyright terms: Public domain W3C validator