Metamath Proof Explorer

Theorem reusv3

Description: Two ways to express single-valuedness of a class expression C ( y ) . See reusv1 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012)

Ref Expression
Hypotheses reusv3.1 ⊢ y = z → φ ↔ ψ
reusv3.2 ⊢ y = z → C = D
Assertion reusv3 ⊢ ∃ y ∈ B φ ∧ C ∈ A → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D ↔ ∃ x ∈ A ∀ y ∈ B φ → x = C

Proof

Step Hyp Ref Expression
1 reusv3.1 ⊢ y = z → φ ↔ ψ
2 reusv3.2 ⊢ y = z → C = D
3 2 eleq1d ⊢ y = z → C ∈ A ↔ D ∈ A
4 1 3 anbi12d ⊢ y = z → φ ∧ C ∈ A ↔ ψ ∧ D ∈ A
5 4 cbvrexvw ⊢ ∃ y ∈ B φ ∧ C ∈ A ↔ ∃ z ∈ B ψ ∧ D ∈ A
6 nfra2w ⊢ Ⅎ z ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D
7 nfv ⊢ Ⅎ z ∃ x ∈ A ∀ y ∈ B φ → x = C
8 6 7 nfim ⊢ Ⅎ z ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∃ x ∈ A ∀ y ∈ B φ → x = C
9 risset ⊢ D ∈ A ↔ ∃ x ∈ A x = D
10 ralcom ⊢ ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D ↔ ∀ z ∈ B ∀ y ∈ B φ ∧ ψ → C = D
11 impexp ⊢ φ ∧ ψ → C = D ↔ φ → ψ → C = D
12 bi2.04 ⊢ φ → ψ → C = D ↔ ψ → φ → C = D
13 11 12 bitri ⊢ φ ∧ ψ → C = D ↔ ψ → φ → C = D
14 13 ralbii ⊢ ∀ y ∈ B φ ∧ ψ → C = D ↔ ∀ y ∈ B ψ → φ → C = D
15 r19.21v ⊢ ∀ y ∈ B ψ → φ → C = D ↔ ψ → ∀ y ∈ B φ → C = D
16 14 15 bitri ⊢ ∀ y ∈ B φ ∧ ψ → C = D ↔ ψ → ∀ y ∈ B φ → C = D
17 16 ralbii ⊢ ∀ z ∈ B ∀ y ∈ B φ ∧ ψ → C = D ↔ ∀ z ∈ B ψ → ∀ y ∈ B φ → C = D
18 10 17 bitri ⊢ ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D ↔ ∀ z ∈ B ψ → ∀ y ∈ B φ → C = D
19 rsp ⊢ ∀ z ∈ B ψ → ∀ y ∈ B φ → C = D → z ∈ B → ψ → ∀ y ∈ B φ → C = D
20 18 19 sylbi ⊢ ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → z ∈ B → ψ → ∀ y ∈ B φ → C = D
21 20 com3l ⊢ z ∈ B → ψ → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∀ y ∈ B φ → C = D
22 21 imp31 ⊢ z ∈ B ∧ ψ ∧ ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∀ y ∈ B φ → C = D
23 eqeq1 ⊢ x = D → x = C ↔ D = C
24 eqcom ⊢ D = C ↔ C = D
25 23 24 bitrdi ⊢ x = D → x = C ↔ C = D
26 25 imbi2d ⊢ x = D → φ → x = C ↔ φ → C = D
27 26 ralbidv ⊢ x = D → ∀ y ∈ B φ → x = C ↔ ∀ y ∈ B φ → C = D
28 22 27 syl5ibrcom ⊢ z ∈ B ∧ ψ ∧ ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → x = D → ∀ y ∈ B φ → x = C
29 28 reximdv ⊢ z ∈ B ∧ ψ ∧ ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∃ x ∈ A x = D → ∃ x ∈ A ∀ y ∈ B φ → x = C
30 29 ex ⊢ z ∈ B ∧ ψ → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∃ x ∈ A x = D → ∃ x ∈ A ∀ y ∈ B φ → x = C
31 30 com23 ⊢ z ∈ B ∧ ψ → ∃ x ∈ A x = D → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∃ x ∈ A ∀ y ∈ B φ → x = C
32 9 31 syl5bi ⊢ z ∈ B ∧ ψ → D ∈ A → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∃ x ∈ A ∀ y ∈ B φ → x = C
33 32 expimpd ⊢ z ∈ B → ψ ∧ D ∈ A → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∃ x ∈ A ∀ y ∈ B φ → x = C
34 8 33 rexlimi ⊢ ∃ z ∈ B ψ ∧ D ∈ A → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∃ x ∈ A ∀ y ∈ B φ → x = C
35 5 34 sylbi ⊢ ∃ y ∈ B φ ∧ C ∈ A → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D → ∃ x ∈ A ∀ y ∈ B φ → x = C
36 1 2 reusv3i ⊢ ∃ x ∈ A ∀ y ∈ B φ → x = C → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D
37 35 36 impbid1 ⊢ ∃ y ∈ B φ ∧ C ∈ A → ∀ y ∈ B ∀ z ∈ B φ ∧ ψ → C = D ↔ ∃ x ∈ A ∀ y ∈ B φ → x = C