Metamath Proof Explorer

Theorem reusv2

Description: Two ways to express single-valuedness of a class expression C ( y ) that is constant for those y e. B such that ph . The first antecedent ensures that the constant value belongs to the existential uniqueness domain A , and the second ensures that C ( y ) is evaluated for at least one y . (Contributed by NM, 4-Jan-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reusv2 ⊢ ∀ y ∈ B φ → C ∈ A ∧ ∃ y ∈ B φ → ∃! x ∈ A ∃ y ∈ B φ ∧ x = C ↔ ∃! x ∈ A ∀ y ∈ B φ → x = C

Proof

Step Hyp Ref Expression
1 nfrab1 ⊢ Ⅎ _ y y ∈ B | φ
2 nfcv ⊢ Ⅎ _ z y ∈ B | φ
3 nfv ⊢ Ⅎ z C ∈ A
4 nfcsb1v ⊢ Ⅎ _ y ⦋ z / y⦌ C
5 4 nfel1 ⊢ Ⅎ y ⦋ z / y⦌ C ∈ A
6 csbeq1a ⊢ y = z → C = ⦋ z / y⦌ C
7 6 eleq1d ⊢ y = z → C ∈ A ↔ ⦋ z / y⦌ C ∈ A
8 1 2 3 5 7 cbvralfw ⊢ ∀ y ∈ y ∈ B | φ C ∈ A ↔ ∀ z ∈ y ∈ B | φ ⦋ z / y⦌ C ∈ A
9 rabid ⊢ y ∈ y ∈ B | φ ↔ y ∈ B ∧ φ
10 9 imbi1i ⊢ y ∈ y ∈ B | φ → C ∈ A ↔ y ∈ B ∧ φ → C ∈ A
11 impexp ⊢ y ∈ B ∧ φ → C ∈ A ↔ y ∈ B → φ → C ∈ A
12 10 11 bitri ⊢ y ∈ y ∈ B | φ → C ∈ A ↔ y ∈ B → φ → C ∈ A
13 12 ralbii2 ⊢ ∀ y ∈ y ∈ B | φ C ∈ A ↔ ∀ y ∈ B φ → C ∈ A
14 8 13 bitr3i ⊢ ∀ z ∈ y ∈ B | φ ⦋ z / y⦌ C ∈ A ↔ ∀ y ∈ B φ → C ∈ A
15 rabn0 ⊢ y ∈ B | φ ≠ ∅ ↔ ∃ y ∈ B φ
16 reusv2lem5 ⊢ ∀ z ∈ y ∈ B | φ ⦋ z / y⦌ C ∈ A ∧ y ∈ B | φ ≠ ∅ → ∃! x ∈ A ∃ z ∈ y ∈ B | φ x = ⦋ z / y⦌ C ↔ ∃! x ∈ A ∀ z ∈ y ∈ B | φ x = ⦋ z / y⦌ C
17 nfv ⊢ Ⅎ z x = C
18 4 nfeq2 ⊢ Ⅎ y x = ⦋ z / y⦌ C
19 6 eqeq2d ⊢ y = z → x = C ↔ x = ⦋ z / y⦌ C
20 1 2 17 18 19 cbvrexfw ⊢ ∃ y ∈ y ∈ B | φ x = C ↔ ∃ z ∈ y ∈ B | φ x = ⦋ z / y⦌ C
21 9 anbi1i ⊢ y ∈ y ∈ B | φ ∧ x = C ↔ y ∈ B ∧ φ ∧ x = C
22 anass ⊢ y ∈ B ∧ φ ∧ x = C ↔ y ∈ B ∧ φ ∧ x = C
23 21 22 bitri ⊢ y ∈ y ∈ B | φ ∧ x = C ↔ y ∈ B ∧ φ ∧ x = C
24 23 rexbii2 ⊢ ∃ y ∈ y ∈ B | φ x = C ↔ ∃ y ∈ B φ ∧ x = C
25 20 24 bitr3i ⊢ ∃ z ∈ y ∈ B | φ x = ⦋ z / y⦌ C ↔ ∃ y ∈ B φ ∧ x = C
26 25 reubii ⊢ ∃! x ∈ A ∃ z ∈ y ∈ B | φ x = ⦋ z / y⦌ C ↔ ∃! x ∈ A ∃ y ∈ B φ ∧ x = C
27 1 2 17 18 19 cbvralfw ⊢ ∀ y ∈ y ∈ B | φ x = C ↔ ∀ z ∈ y ∈ B | φ x = ⦋ z / y⦌ C
28 9 imbi1i ⊢ y ∈ y ∈ B | φ → x = C ↔ y ∈ B ∧ φ → x = C
29 impexp ⊢ y ∈ B ∧ φ → x = C ↔ y ∈ B → φ → x = C
30 28 29 bitri ⊢ y ∈ y ∈ B | φ → x = C ↔ y ∈ B → φ → x = C
31 30 ralbii2 ⊢ ∀ y ∈ y ∈ B | φ x = C ↔ ∀ y ∈ B φ → x = C
32 27 31 bitr3i ⊢ ∀ z ∈ y ∈ B | φ x = ⦋ z / y⦌ C ↔ ∀ y ∈ B φ → x = C
33 32 reubii ⊢ ∃! x ∈ A ∀ z ∈ y ∈ B | φ x = ⦋ z / y⦌ C ↔ ∃! x ∈ A ∀ y ∈ B φ → x = C
34 16 26 33 3bitr3g ⊢ ∀ z ∈ y ∈ B | φ ⦋ z / y⦌ C ∈ A ∧ y ∈ B | φ ≠ ∅ → ∃! x ∈ A ∃ y ∈ B φ ∧ x = C ↔ ∃! x ∈ A ∀ y ∈ B φ → x = C
35 14 15 34 syl2anbr ⊢ ∀ y ∈ B φ → C ∈ A ∧ ∃ y ∈ B φ → ∃! x ∈ A ∃ y ∈ B φ ∧ x = C ↔ ∃! x ∈ A ∀ y ∈ B φ → x = C