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 ⊢Ⅎ_yy∈B|φ
2 nfcv ⊢Ⅎ_zy∈B|φ
3 nfv ⊢ℲzC∈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 ⊢Ⅎzx=C
18 4 nfeq2 ⊢Ⅎyx=⦋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