Metamath Proof Explorer

Theorem reuprg0

Description: Convert a restricted existential uniqueness over a pair to a disjunction of conjunctions. (Contributed by AV, 2-Apr-2023)

Ref Expression
Hypotheses reuprg.1 ⊢ x = A → φ ↔ ψ
reuprg.2 ⊢ x = B → φ ↔ χ
Assertion reuprg0 ⊢ A ∈ V ∧ B ∈ W → ∃! x ∈ A B φ ↔ ψ ∧ χ → A = B ∨ χ ∧ ψ → A = B

Proof

Step Hyp Ref Expression
1 reuprg.1 ⊢ x = A → φ ↔ ψ
2 reuprg.2 ⊢ x = B → φ ↔ χ
3 nfsbc1v ⊢ Ⅎ x [˙c / x]˙ φ
4 nfsbc1v ⊢ Ⅎ x [˙w / x]˙ φ
5 sbceq1a ⊢ x = w → φ ↔ [˙w / x]˙ φ
6 dfsbcq ⊢ w = c → [˙w / x]˙ φ ↔ [˙c / x]˙ φ
7 3 4 5 6 reu8nf ⊢ ∃! x ∈ A B φ ↔ ∃ x ∈ A B φ ∧ ∀ c ∈ A B [˙c / x]˙ φ → x = c
8 nfv ⊢ Ⅎ x ψ
9 nfcv ⊢ Ⅎ _ x A B
10 nfv ⊢ Ⅎ x A = c
11 3 10 nfim ⊢ Ⅎ x [˙c / x]˙ φ → A = c
12 9 11 nfralw ⊢ Ⅎ x ∀ c ∈ A B [˙c / x]˙ φ → A = c
13 8 12 nfan ⊢ Ⅎ x ψ ∧ ∀ c ∈ A B [˙c / x]˙ φ → A = c
14 nfv ⊢ Ⅎ x χ
15 nfv ⊢ Ⅎ x B = c
16 3 15 nfim ⊢ Ⅎ x [˙c / x]˙ φ → B = c
17 9 16 nfralw ⊢ Ⅎ x ∀ c ∈ A B [˙c / x]˙ φ → B = c
18 14 17 nfan ⊢ Ⅎ x χ ∧ ∀ c ∈ A B [˙c / x]˙ φ → B = c
19 eqeq1 ⊢ x = A → x = c ↔ A = c
20 19 imbi2d ⊢ x = A → [˙c / x]˙ φ → x = c ↔ [˙c / x]˙ φ → A = c
21 20 ralbidv ⊢ x = A → ∀ c ∈ A B [˙c / x]˙ φ → x = c ↔ ∀ c ∈ A B [˙c / x]˙ φ → A = c
22 1 21 anbi12d ⊢ x = A → φ ∧ ∀ c ∈ A B [˙c / x]˙ φ → x = c ↔ ψ ∧ ∀ c ∈ A B [˙c / x]˙ φ → A = c
23 eqeq1 ⊢ x = B → x = c ↔ B = c
24 23 imbi2d ⊢ x = B → [˙c / x]˙ φ → x = c ↔ [˙c / x]˙ φ → B = c
25 24 ralbidv ⊢ x = B → ∀ c ∈ A B [˙c / x]˙ φ → x = c ↔ ∀ c ∈ A B [˙c / x]˙ φ → B = c
26 2 25 anbi12d ⊢ x = B → φ ∧ ∀ c ∈ A B [˙c / x]˙ φ → x = c ↔ χ ∧ ∀ c ∈ A B [˙c / x]˙ φ → B = c
27 13 18 22 26 rexprgf ⊢ A ∈ V ∧ B ∈ W → ∃ x ∈ A B φ ∧ ∀ c ∈ A B [˙c / x]˙ φ → x = c ↔ ψ ∧ ∀ c ∈ A B [˙c / x]˙ φ → A = c ∨ χ ∧ ∀ c ∈ A B [˙c / x]˙ φ → B = c
28 dfsbcq ⊢ c = A → [˙c / x]˙ φ ↔ [˙A / x]˙ φ
29 eqeq2 ⊢ c = A → A = c ↔ A = A
30 28 29 imbi12d ⊢ c = A → [˙c / x]˙ φ → A = c ↔ [˙A / x]˙ φ → A = A
31 dfsbcq ⊢ c = B → [˙c / x]˙ φ ↔ [˙B / x]˙ φ
32 eqeq2 ⊢ c = B → A = c ↔ A = B
33 31 32 imbi12d ⊢ c = B → [˙c / x]˙ φ → A = c ↔ [˙B / x]˙ φ → A = B
34 30 33 ralprg ⊢ A ∈ V ∧ B ∈ W → ∀ c ∈ A B [˙c / x]˙ φ → A = c ↔ [˙A / x]˙ φ → A = A ∧ [˙B / x]˙ φ → A = B
35 eqidd ⊢ [˙A / x]˙ φ → A = A
36 35 biantrur ⊢ [˙B / x]˙ φ → A = B ↔ [˙A / x]˙ φ → A = A ∧ [˙B / x]˙ φ → A = B
37 2 sbcieg ⊢ B ∈ W → [˙B / x]˙ φ ↔ χ
38 37 adantl ⊢ A ∈ V ∧ B ∈ W → [˙B / x]˙ φ ↔ χ
39 38 imbi1d ⊢ A ∈ V ∧ B ∈ W → [˙B / x]˙ φ → A = B ↔ χ → A = B
40 36 39 bitr3id ⊢ A ∈ V ∧ B ∈ W → [˙A / x]˙ φ → A = A ∧ [˙B / x]˙ φ → A = B ↔ χ → A = B
41 34 40 bitrd ⊢ A ∈ V ∧ B ∈ W → ∀ c ∈ A B [˙c / x]˙ φ → A = c ↔ χ → A = B
42 41 anbi2d ⊢ A ∈ V ∧ B ∈ W → ψ ∧ ∀ c ∈ A B [˙c / x]˙ φ → A = c ↔ ψ ∧ χ → A = B
43 eqeq2 ⊢ c = A → B = c ↔ B = A
44 28 43 imbi12d ⊢ c = A → [˙c / x]˙ φ → B = c ↔ [˙A / x]˙ φ → B = A
45 eqeq2 ⊢ c = B → B = c ↔ B = B
46 31 45 imbi12d ⊢ c = B → [˙c / x]˙ φ → B = c ↔ [˙B / x]˙ φ → B = B
47 44 46 ralprg ⊢ A ∈ V ∧ B ∈ W → ∀ c ∈ A B [˙c / x]˙ φ → B = c ↔ [˙A / x]˙ φ → B = A ∧ [˙B / x]˙ φ → B = B
48 eqidd ⊢ [˙B / x]˙ φ → B = B
49 48 biantru ⊢ [˙A / x]˙ φ → B = A ↔ [˙A / x]˙ φ → B = A ∧ [˙B / x]˙ φ → B = B
50 1 sbcieg ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ
51 50 adantr ⊢ A ∈ V ∧ B ∈ W → [˙A / x]˙ φ ↔ ψ
52 51 imbi1d ⊢ A ∈ V ∧ B ∈ W → [˙A / x]˙ φ → B = A ↔ ψ → B = A
53 49 52 bitr3id ⊢ A ∈ V ∧ B ∈ W → [˙A / x]˙ φ → B = A ∧ [˙B / x]˙ φ → B = B ↔ ψ → B = A
54 47 53 bitrd ⊢ A ∈ V ∧ B ∈ W → ∀ c ∈ A B [˙c / x]˙ φ → B = c ↔ ψ → B = A
55 54 anbi2d ⊢ A ∈ V ∧ B ∈ W → χ ∧ ∀ c ∈ A B [˙c / x]˙ φ → B = c ↔ χ ∧ ψ → B = A
56 eqcom ⊢ B = A ↔ A = B
57 56 imbi2i ⊢ ψ → B = A ↔ ψ → A = B
58 57 anbi2i ⊢ χ ∧ ψ → B = A ↔ χ ∧ ψ → A = B
59 55 58 bitrdi ⊢ A ∈ V ∧ B ∈ W → χ ∧ ∀ c ∈ A B [˙c / x]˙ φ → B = c ↔ χ ∧ ψ → A = B
60 42 59 orbi12d ⊢ A ∈ V ∧ B ∈ W → ψ ∧ ∀ c ∈ A B [˙c / x]˙ φ → A = c ∨ χ ∧ ∀ c ∈ A B [˙c / x]˙ φ → B = c ↔ ψ ∧ χ → A = B ∨ χ ∧ ψ → A = B
61 27 60 bitrd ⊢ A ∈ V ∧ B ∈ W → ∃ x ∈ A B φ ∧ ∀ c ∈ A B [˙c / x]˙ φ → x = c ↔ ψ ∧ χ → A = B ∨ χ ∧ ψ → A = B
62 7 61 syl5bb ⊢ A ∈ V ∧ B ∈ W → ∃! x ∈ A B φ ↔ ψ ∧ χ → A = B ∨ χ ∧ ψ → A = B