Metamath Proof Explorer

Theorem reusv2lem4

Description: Lemma for reusv2 . (Contributed by NM, 13-Dec-2012)

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

Proof

Step Hyp Ref Expression
1 df-reu ⊢∃!x∈A∃y∈Bφ∧x=C↔∃!xx∈A∧∃y∈Bφ∧x=C
2 anass ⊢y∈B∧C∈A∧φ∧x=C↔y∈B∧C∈A∧φ∧x=C
3 rabid ⊢y∈y∈B|C∈A∧φ↔y∈B∧C∈A∧φ
4 3 anbi1i ⊢y∈y∈B|C∈A∧φ∧x=C↔y∈B∧C∈A∧φ∧x=C
5 anass ⊢x∈A∧φ∧x=C↔x∈A∧φ∧x=C
6 eleq1 ⊢x=C→x∈A↔C∈A
7 6 anbi1d ⊢x=C→x∈A∧φ↔C∈A∧φ
8 7 pm5.32ri ⊢x∈A∧φ∧x=C↔C∈A∧φ∧x=C
9 5 8 bitr3i ⊢x∈A∧φ∧x=C↔C∈A∧φ∧x=C
10 9 anbi2i ⊢y∈B∧x∈A∧φ∧x=C↔y∈B∧C∈A∧φ∧x=C
11 2 4 10 3bitr4ri ⊢y∈B∧x∈A∧φ∧x=C↔y∈y∈B|C∈A∧φ∧x=C
12 11 rexbii2 ⊢∃y∈Bx∈A∧φ∧x=C↔∃y∈y∈B|C∈A∧φx=C
13 r19.42v ⊢∃y∈Bx∈A∧φ∧x=C↔x∈A∧∃y∈Bφ∧x=C
14 nfrab1 ⊢Ⅎ_yy∈B|C∈A∧φ
15 nfcv ⊢Ⅎ_zy∈B|C∈A∧φ
16 nfv ⊢Ⅎzx=C
17 nfcsb1v ⊢Ⅎ_y⦋z/y⦌C
18 17 nfeq2 ⊢Ⅎyx=⦋z/y⦌C
19 csbeq1a ⊢y=z→C=⦋z/y⦌C
20 19 eqeq2d ⊢y=z→x=C↔x=⦋z/y⦌C
21 14 15 16 18 20 cbvrexfw ⊢∃y∈y∈B|C∈A∧φx=C↔∃z∈y∈B|C∈A∧φx=⦋z/y⦌C
22 12 13 21 3bitr3i ⊢x∈A∧∃y∈Bφ∧x=C↔∃z∈y∈B|C∈A∧φx=⦋z/y⦌C
23 22 eubii ⊢∃!xx∈A∧∃y∈Bφ∧x=C↔∃!x∃z∈y∈B|C∈A∧φx=⦋z/y⦌C
24 elex ⊢C∈A→C∈V
25 24 ad2antrl ⊢y∈B∧C∈A∧φ→C∈V
26 3 25 sylbi ⊢y∈y∈B|C∈A∧φ→C∈V
27 26 rgen ⊢∀y∈y∈B|C∈A∧φC∈V
28 nfv ⊢ℲzC∈V
29 17 nfel1 ⊢Ⅎy⦋z/y⦌C∈V
30 19 eleq1d ⊢y=z→C∈V↔⦋z/y⦌C∈V
31 14 15 28 29 30 cbvralfw ⊢∀y∈y∈B|C∈A∧φC∈V↔∀z∈y∈B|C∈A∧φ⦋z/y⦌C∈V
32 27 31 mpbi ⊢∀z∈y∈B|C∈A∧φ⦋z/y⦌C∈V
33 reusv2lem3 ⊢∀z∈y∈B|C∈A∧φ⦋z/y⦌C∈V→∃!x∃z∈y∈B|C∈A∧φx=⦋z/y⦌C↔∃!x∀z∈y∈B|C∈A∧φx=⦋z/y⦌C
34 32 33 ax-mp ⊢∃!x∃z∈y∈B|C∈A∧φx=⦋z/y⦌C↔∃!x∀z∈y∈B|C∈A∧φx=⦋z/y⦌C
35 df-ral ⊢∀z∈y∈B|C∈A∧φx=⦋z/y⦌C↔∀zz∈y∈B|C∈A∧φ→x=⦋z/y⦌C
36 nfv ⊢Ⅎzy∈y∈B|C∈A∧φ→x=C
37 14 nfcri ⊢Ⅎyz∈y∈B|C∈A∧φ
38 37 18 nfim ⊢Ⅎyz∈y∈B|C∈A∧φ→x=⦋z/y⦌C
39 eleq1 ⊢y=z→y∈y∈B|C∈A∧φ↔z∈y∈B|C∈A∧φ
40 39 20 imbi12d ⊢y=z→y∈y∈B|C∈A∧φ→x=C↔z∈y∈B|C∈A∧φ→x=⦋z/y⦌C
41 36 38 40 cbvalv1 ⊢∀yy∈y∈B|C∈A∧φ→x=C↔∀zz∈y∈B|C∈A∧φ→x=⦋z/y⦌C
42 3 imbi1i ⊢y∈y∈B|C∈A∧φ→x=C↔y∈B∧C∈A∧φ→x=C
43 impexp ⊢y∈B∧C∈A∧φ→x=C↔y∈B→C∈A∧φ→x=C
44 42 43 bitri ⊢y∈y∈B|C∈A∧φ→x=C↔y∈B→C∈A∧φ→x=C
45 44 albii ⊢∀yy∈y∈B|C∈A∧φ→x=C↔∀yy∈B→C∈A∧φ→x=C
46 df-ral ⊢∀y∈BC∈A∧φ→x=C↔∀yy∈B→C∈A∧φ→x=C
47 45 46 bitr4i ⊢∀yy∈y∈B|C∈A∧φ→x=C↔∀y∈BC∈A∧φ→x=C
48 35 41 47 3bitr2i ⊢∀z∈y∈B|C∈A∧φx=⦋z/y⦌C↔∀y∈BC∈A∧φ→x=C
49 48 eubii ⊢∃!x∀z∈y∈B|C∈A∧φx=⦋z/y⦌C↔∃!x∀y∈BC∈A∧φ→x=C
50 34 49 bitri ⊢∃!x∃z∈y∈B|C∈A∧φx=⦋z/y⦌C↔∃!x∀y∈BC∈A∧φ→x=C
51 1 23 50 3bitri ⊢∃!x∈A∃y∈Bφ∧x=C↔∃!x∀y∈BC∈A∧φ→x=C