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

Theorem reuprg0 4707
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 3811 . . 3 𝑥[𝑐 / 𝑥]𝜑
2 nfsbc1v 3811 . . 3 𝑥[𝑤 / 𝑥]𝜑
3 sbceq1a 3802 . . 3 (𝑥 = 𝑤 → (𝜑[𝑤 / 𝑥]𝜑))
4 dfsbcq 3793 . . 3 (𝑤 = 𝑐 → ([𝑤 / 𝑥]𝜑[𝑐 / 𝑥]𝜑))
51, 2, 3, 4reu8nf 3886 . 2 (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∃𝑥 ∈ {𝐴, 𝐵} (𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)))
6 nfv 1912 . . . . 5 𝑥𝜓
7 nfcv 2903 . . . . . 6 𝑥{𝐴, 𝐵}
8 nfv 1912 . . . . . . 7 𝑥 𝐴 = 𝑐
91, 8nfim 1894 . . . . . 6 𝑥([𝑐 / 𝑥]𝜑𝐴 = 𝑐)
107, 9nfralw 3309 . . . . 5 𝑥𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)
116, 10nfan 1897 . . . 4 𝑥(𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐))
12 nfv 1912 . . . . 5 𝑥𝜒
13 nfv 1912 . . . . . . 7 𝑥 𝐵 = 𝑐
141, 13nfim 1894 . . . . . 6 𝑥([𝑐 / 𝑥]𝜑𝐵 = 𝑐)
157, 14nfralw 3309 . . . . 5 𝑥𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)
1612, 15nfan 1897 . . . 4 𝑥(𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐))
17 reuprg.1 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
18 eqeq1 2739 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 = 𝑐𝐴 = 𝑐))
1918imbi2d 340 . . . . . 6 (𝑥 = 𝐴 → (([𝑐 / 𝑥]𝜑𝑥 = 𝑐) ↔ ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)))
2019ralbidv 3176 . . . . 5 (𝑥 = 𝐴 → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐) ↔ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)))
2117, 20anbi12d 632 . . . 4 (𝑥 = 𝐴 → ((𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)) ↔ (𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐))))
22 reuprg.2 . . . . 5 (𝑥 = 𝐵 → (𝜑𝜒))
23 eqeq1 2739 . . . . . . 7 (𝑥 = 𝐵 → (𝑥 = 𝑐𝐵 = 𝑐))
2423imbi2d 340 . . . . . 6 (𝑥 = 𝐵 → (([𝑐 / 𝑥]𝜑𝑥 = 𝑐) ↔ ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)))
2524ralbidv 3176 . . . . 5 (𝑥 = 𝐵 → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐) ↔ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)))
2622, 25anbi12d 632 . . . 4 (𝑥 = 𝐵 → ((𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)) ↔ (𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐))))
2711, 16, 21, 26rexprgf 4700 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑥 ∈ {𝐴, 𝐵} (𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)) ↔ ((𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)) ∨ (𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)))))
28 dfsbcq 3793 . . . . . . . 8 (𝑐 = 𝐴 → ([𝑐 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
29 eqeq2 2747 . . . . . . . 8 (𝑐 = 𝐴 → (𝐴 = 𝑐𝐴 = 𝐴))
3028, 29imbi12d 344 . . . . . . 7 (𝑐 = 𝐴 → (([𝑐 / 𝑥]𝜑𝐴 = 𝑐) ↔ ([𝐴 / 𝑥]𝜑𝐴 = 𝐴)))
31 dfsbcq 3793 . . . . . . . 8 (𝑐 = 𝐵 → ([𝑐 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
32 eqeq2 2747 . . . . . . . 8 (𝑐 = 𝐵 → (𝐴 = 𝑐𝐴 = 𝐵))
3331, 32imbi12d 344 . . . . . . 7 (𝑐 = 𝐵 → (([𝑐 / 𝑥]𝜑𝐴 = 𝑐) ↔ ([𝐵 / 𝑥]𝜑𝐴 = 𝐵)))
3430, 33ralprg 4701 . . . . . 6 ((𝐴𝑉𝐵𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐) ↔ (([𝐴 / 𝑥]𝜑𝐴 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐴 = 𝐵))))
35 eqidd 2736 . . . . . . . 8 ([𝐴 / 𝑥]𝜑𝐴 = 𝐴)
3635biantrur 530 . . . . . . 7 (([𝐵 / 𝑥]𝜑𝐴 = 𝐵) ↔ (([𝐴 / 𝑥]𝜑𝐴 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐴 = 𝐵)))
3722sbcieg 3832 . . . . . . . . 9 (𝐵𝑊 → ([𝐵 / 𝑥]𝜑𝜒))
3837adantl 481 . . . . . . . 8 ((𝐴𝑉𝐵𝑊) → ([𝐵 / 𝑥]𝜑𝜒))
3938imbi1d 341 . . . . . . 7 ((𝐴𝑉𝐵𝑊) → (([𝐵 / 𝑥]𝜑𝐴 = 𝐵) ↔ (𝜒𝐴 = 𝐵)))
4036, 39bitr3id 285 . . . . . 6 ((𝐴𝑉𝐵𝑊) → ((([𝐴 / 𝑥]𝜑𝐴 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐴 = 𝐵)) ↔ (𝜒𝐴 = 𝐵)))
4134, 40bitrd 279 . . . . 5 ((𝐴𝑉𝐵𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐) ↔ (𝜒𝐴 = 𝐵)))
4241anbi2d 630 . . . 4 ((𝐴𝑉𝐵𝑊) → ((𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)) ↔ (𝜓 ∧ (𝜒𝐴 = 𝐵))))
43 eqeq2 2747 . . . . . . . . 9 (𝑐 = 𝐴 → (𝐵 = 𝑐𝐵 = 𝐴))
4428, 43imbi12d 344 . . . . . . . 8 (𝑐 = 𝐴 → (([𝑐 / 𝑥]𝜑𝐵 = 𝑐) ↔ ([𝐴 / 𝑥]𝜑𝐵 = 𝐴)))
45 eqeq2 2747 . . . . . . . . 9 (𝑐 = 𝐵 → (𝐵 = 𝑐𝐵 = 𝐵))
4631, 45imbi12d 344 . . . . . . . 8 (𝑐 = 𝐵 → (([𝑐 / 𝑥]𝜑𝐵 = 𝑐) ↔ ([𝐵 / 𝑥]𝜑𝐵 = 𝐵)))
4744, 46ralprg 4701 . . . . . . 7 ((𝐴𝑉𝐵𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐) ↔ (([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐵 = 𝐵))))
48 eqidd 2736 . . . . . . . . 9 ([𝐵 / 𝑥]𝜑𝐵 = 𝐵)
4948biantru 529 . . . . . . . 8 (([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ↔ (([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐵 = 𝐵)))
5017sbcieg 3832 . . . . . . . . . 10 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
5150adantr 480 . . . . . . . . 9 ((𝐴𝑉𝐵𝑊) → ([𝐴 / 𝑥]𝜑𝜓))
5251imbi1d 341 . . . . . . . 8 ((𝐴𝑉𝐵𝑊) → (([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ↔ (𝜓𝐵 = 𝐴)))
5349, 52bitr3id 285 . . . . . . 7 ((𝐴𝑉𝐵𝑊) → ((([𝐴 / 𝑥]𝜑𝐵 = 𝐴) ∧ ([𝐵 / 𝑥]𝜑𝐵 = 𝐵)) ↔ (𝜓𝐵 = 𝐴)))
5447, 53bitrd 279 . . . . . 6 ((𝐴𝑉𝐵𝑊) → (∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐) ↔ (𝜓𝐵 = 𝐴)))
5554anbi2d 630 . . . . 5 ((𝐴𝑉𝐵𝑊) → ((𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)) ↔ (𝜒 ∧ (𝜓𝐵 = 𝐴))))
56 eqcom 2742 . . . . . . 7 (𝐵 = 𝐴𝐴 = 𝐵)
5756imbi2i 336 . . . . . 6 ((𝜓𝐵 = 𝐴) ↔ (𝜓𝐴 = 𝐵))
5857anbi2i 623 . . . . 5 ((𝜒 ∧ (𝜓𝐵 = 𝐴)) ↔ (𝜒 ∧ (𝜓𝐴 = 𝐵)))
5955, 58bitrdi 287 . . . 4 ((𝐴𝑉𝐵𝑊) → ((𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐)) ↔ (𝜒 ∧ (𝜓𝐴 = 𝐵))))
6042, 59orbi12d 918 . . 3 ((𝐴𝑉𝐵𝑊) → (((𝜓 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐴 = 𝑐)) ∨ (𝜒 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝐵 = 𝑐))) ↔ ((𝜓 ∧ (𝜒𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓𝐴 = 𝐵)))))
6127, 60bitrd 279 . 2 ((𝐴𝑉𝐵𝑊) → (∃𝑥 ∈ {𝐴, 𝐵} (𝜑 ∧ ∀𝑐 ∈ {𝐴, 𝐵} ([𝑐 / 𝑥]𝜑𝑥 = 𝑐)) ↔ ((𝜓 ∧ (𝜒𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓𝐴 = 𝐵)))))
625, 61bitrid 283 1 ((𝐴𝑉𝐵𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∧ (𝜒𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓𝐴 = 𝐵)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847   = wceq 1537  wcel 2106  wral 3059  wrex 3068  ∃!wreu 3376  [wsbc 3791  {cpr 4633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-v 3480  df-sbc 3792  df-un 3968  df-sn 4632  df-pr 4634
This theorem is referenced by:  reuprg  4708
  Copyright terms: Public domain W3C validator