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

Theorem reuprg0 4600
 Description: Convert a restricted existential uniqueness over a pair to a disjunction of conjunctions. (Contributed by AV, 2-Apr-2023.)
Hypotheses
Ref Expression
reuprg.1 (𝑥 = 𝐴 → (𝜑𝜓))
reuprg.2 (𝑥 = 𝐵 → (𝜑𝜒))
Assertion
Ref Expression
reuprg0 ((𝐴𝑉𝐵𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∧ (𝜒𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓𝐴 = 𝐵)))))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem reuprg0
Dummy variables 𝑤 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfsbc1v 3741 . . 3 𝑥[𝑐 / 𝑥]𝜑
2 nfsbc1v 3741 . . 3 𝑥[𝑤 / 𝑥]𝜑
3 sbceq1a 3732 . . 3 (𝑥 = 𝑤 → (𝜑[𝑤 / 𝑥]𝜑))
4 dfsbcq 3723 . . 3 (𝑤 = 𝑐 → ([𝑤 / 𝑥]𝜑[𝑐 / 𝑥]𝜑))
51, 2, 3, 4reu8nf 3807 . 2 (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∃𝑥 ∈ {𝐴, 𝐵} (𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)))
6 nfv 1915 . . . . 5 𝑥𝜓
7 nfcv 2955 . . . . . 6 𝑥{𝐴, 𝐵}
8 nfv 1915 . . . . . . 7 𝑥 𝐴 = 𝑐
91, 8nfim 1897 . . . . . 6 𝑥([𝑐 / 𝑥]𝜑𝐴 = 𝑐)
107, 9nfralw 3189 . . . . 5 𝑥𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)
116, 10nfan 1900 . . . 4 𝑥(𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐))
12 nfv 1915 . . . . 5 𝑥𝜒
13 nfv 1915 . . . . . . 7 𝑥 𝐵 = 𝑐
141, 13nfim 1897 . . . . . 6 𝑥([𝑐 / 𝑥]𝜑𝐵 = 𝑐)
157, 14nfralw 3189 . . . . 5 𝑥𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)
1612, 15nfan 1900 . . . 4 𝑥(𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐))
17 reuprg.1 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
18 eqeq1 2802 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 = 𝑐𝐴 = 𝑐))
1918imbi2d 344 . . . . . 6 (𝑥 = 𝐴 → (([𝑐 / 𝑥]𝜑𝑥 = 𝑐) ↔ ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)))
2019ralbidv 3162 . . . . 5 (𝑥 = 𝐴 → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐) ↔ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)))
2117, 20anbi12d 633 . . . 4 (𝑥 = 𝐴 → ((𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)) ↔ (𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐))))
22 reuprg.2 . . . . 5 (𝑥 = 𝐵 → (𝜑𝜒))
23 eqeq1 2802 . . . . . . 7 (𝑥 = 𝐵 → (𝑥 = 𝑐𝐵 = 𝑐))
2423imbi2d 344 . . . . . 6 (𝑥 = 𝐵 → (([𝑐 / 𝑥]𝜑𝑥 = 𝑐) ↔ ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)))
2524ralbidv 3162 . . . . 5 (𝑥 = 𝐵 → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐) ↔ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)))
2622, 25anbi12d 633 . . . 4 (𝑥 = 𝐵 → ((𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)) ↔ (𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐))))
2711, 16, 21, 26rexprgf 4593 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑥 ∈ {𝐴, 𝐵} (𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)) ↔ ((𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)) ∨ (𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)))))
28 dfsbcq 3723 . . . . . . . 8 (𝑐 = 𝐴 → ([𝑐 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
29 eqeq2 2810 . . . . . . . 8 (𝑐 = 𝐴 → (𝐴 = 𝑐𝐴 = 𝐴))
3028, 29imbi12d 348 . . . . . . 7 (𝑐 = 𝐴 → (([𝑐 / 𝑥]𝜑𝐴 = 𝑐) ↔ ([𝐴 / 𝑥]𝜑𝐴 = 𝐴)))
31 dfsbcq 3723 . . . . . . . 8 (𝑐 = 𝐵 → ([𝑐 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
32 eqeq2 2810 . . . . . . . 8 (𝑐 = 𝐵 → (𝐴 = 𝑐𝐴 = 𝐵))
3331, 32imbi12d 348 . . . . . . 7 (𝑐 = 𝐵 → (([𝑐 / 𝑥]𝜑𝐴 = 𝑐) ↔ ([𝐵 / 𝑥]𝜑𝐴 = 𝐵)))
3430, 33ralprg 4594 . . . . . 6 ((𝐴𝑉𝐵𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐) ↔ (([𝐴 / 𝑥]𝜑𝐴 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐴 = 𝐵))))
35 eqidd 2799 . . . . . . . 8 ([𝐴 / 𝑥]𝜑𝐴 = 𝐴)
3635biantrur 534 . . . . . . 7 (([𝐵 / 𝑥]𝜑𝐴 = 𝐵) ↔ (([𝐴 / 𝑥]𝜑𝐴 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐴 = 𝐵)))
3722sbcieg 3759 . . . . . . . . 9 (𝐵𝑊 → ([𝐵 / 𝑥]𝜑𝜒))
3837adantl 485 . . . . . . . 8 ((𝐴𝑉𝐵𝑊) → ([𝐵 / 𝑥]𝜑𝜒))
3938imbi1d 345 . . . . . . 7 ((𝐴𝑉𝐵𝑊) → (([𝐵 / 𝑥]𝜑𝐴 = 𝐵) ↔ (𝜒𝐴 = 𝐵)))
4036, 39bitr3id 288 . . . . . 6 ((𝐴𝑉𝐵𝑊) → ((([𝐴 / 𝑥]𝜑𝐴 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐴 = 𝐵)) ↔ (𝜒𝐴 = 𝐵)))
4134, 40bitrd 282 . . . . 5 ((𝐴𝑉𝐵𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐) ↔ (𝜒𝐴 = 𝐵)))
4241anbi2d 631 . . . 4 ((𝐴𝑉𝐵𝑊) → ((𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)) ↔ (𝜓 ∧ (𝜒𝐴 = 𝐵))))
43 eqeq2 2810 . . . . . . . . 9 (𝑐 = 𝐴 → (𝐵 = 𝑐𝐵 = 𝐴))
4428, 43imbi12d 348 . . . . . . . 8 (𝑐 = 𝐴 → (([𝑐 / 𝑥]𝜑𝐵 = 𝑐) ↔ ([𝐴 / 𝑥]𝜑𝐵 = 𝐴)))
45 eqeq2 2810 . . . . . . . . 9 (𝑐 = 𝐵 → (𝐵 = 𝑐𝐵 = 𝐵))
4631, 45imbi12d 348 . . . . . . . 8 (𝑐 = 𝐵 → (([𝑐 / 𝑥]𝜑𝐵 = 𝑐) ↔ ([𝐵 / 𝑥]𝜑𝐵 = 𝐵)))
4744, 46ralprg 4594 . . . . . . 7 ((𝐴𝑉𝐵𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐) ↔ (([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐵 = 𝐵))))
48 eqidd 2799 . . . . . . . . 9 ([𝐵 / 𝑥]𝜑𝐵 = 𝐵)
4948biantru 533 . . . . . . . 8 (([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ↔ (([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐵 = 𝐵)))
5017sbcieg 3759 . . . . . . . . . 10 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
5150adantr 484 . . . . . . . . 9 ((𝐴𝑉𝐵𝑊) → ([𝐴 / 𝑥]𝜑𝜓))
5251imbi1d 345 . . . . . . . 8 ((𝐴𝑉𝐵𝑊) → (([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ↔ (𝜓𝐵 = 𝐴)))
5349, 52bitr3id 288 . . . . . . 7 ((𝐴𝑉𝐵𝑊) → ((([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐵 = 𝐵)) ↔ (𝜓𝐵 = 𝐴)))
5447, 53bitrd 282 . . . . . 6 ((𝐴𝑉𝐵𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐) ↔ (𝜓𝐵 = 𝐴)))
5554anbi2d 631 . . . . 5 ((𝐴𝑉𝐵𝑊) → ((𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)) ↔ (𝜒 ∧ (𝜓𝐵 = 𝐴))))
56 eqcom 2805 . . . . . . 7 (𝐵 = 𝐴𝐴 = 𝐵)
5756imbi2i 339 . . . . . 6 ((𝜓𝐵 = 𝐴) ↔ (𝜓𝐴 = 𝐵))
5857anbi2i 625 . . . . 5 ((𝜒 ∧ (𝜓𝐵 = 𝐴)) ↔ (𝜒 ∧ (𝜓𝐴 = 𝐵)))
5955, 58syl6bb 290 . . . 4 ((𝐴𝑉𝐵𝑊) → ((𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)) ↔ (𝜒 ∧ (𝜓𝐴 = 𝐵))))
6042, 59orbi12d 916 . . 3 ((𝐴𝑉𝐵𝑊) → (((𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)) ∨ (𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐))) ↔ ((𝜓 ∧ (𝜒𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓𝐴 = 𝐵)))))
6127, 60bitrd 282 . 2 ((𝐴𝑉𝐵𝑊) → (∃𝑥 ∈ {𝐴, 𝐵} (𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)) ↔ ((𝜓 ∧ (𝜒𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓𝐴 = 𝐵)))))
625, 61syl5bb 286 1 ((𝐴𝑉𝐵𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∧ (𝜒𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓𝐴 = 𝐵)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  ∃!wreu 3108  [wsbc 3721  {cpr 4529 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-reu 3113  df-v 3443  df-sbc 3722  df-un 3887  df-sn 4528  df-pr 4530 This theorem is referenced by:  reuprg  4601
 Copyright terms: Public domain W3C validator