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 ∈ B C ∈ A ∧ φ → x = C

Proof

Step Hyp Ref Expression
1 df-reu ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ x = C ↔ ∃! x x ∈ 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 ∈ B x ∈ A ∧ φ ∧ x = C ↔ ∃ y ∈ y ∈ B | C ∈ A ∧ φ x = C
13 r19.42v ⊢ ∃ y ∈ B x ∈ A ∧ φ ∧ x = C ↔ x ∈ A ∧ ∃ y ∈ B φ ∧ x = C
14 nfrab1 ⊢ Ⅎ _ y y ∈ B | C ∈ A ∧ φ
15 nfcv ⊢ Ⅎ _ z y ∈ B | C ∈ A ∧ φ
16 nfv ⊢ Ⅎ z x = C
17 nfcsb1v ⊢ Ⅎ _ y ⦋ z / y⦌ C
18 17 nfeq2 ⊢ Ⅎ y x = ⦋ 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 ⊢ ∃! x x ∈ 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 ⊢ Ⅎ z C ∈ 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 ↔ ∀ z z ∈ y ∈ B | C ∈ A ∧ φ → x = ⦋ z / y⦌ C
36 nfv ⊢ Ⅎ z y ∈ y ∈ B | C ∈ A ∧ φ → x = C
37 14 nfcri ⊢ Ⅎ y z ∈ y ∈ B | C ∈ A ∧ φ
38 37 18 nfim ⊢ Ⅎ y z ∈ 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 ⊢ ∀ y y ∈ y ∈ B | C ∈ A ∧ φ → x = C ↔ ∀ z z ∈ 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 ⊢ ∀ y y ∈ y ∈ B | C ∈ A ∧ φ → x = C ↔ ∀ y y ∈ B → C ∈ A ∧ φ → x = C
46 df-ral ⊢ ∀ y ∈ B C ∈ A ∧ φ → x = C ↔ ∀ y y ∈ B → C ∈ A ∧ φ → x = C
47 45 46 bitr4i ⊢ ∀ y y ∈ y ∈ B | C ∈ A ∧ φ → x = C ↔ ∀ y ∈ B C ∈ A ∧ φ → x = C
48 35 41 47 3bitr2i ⊢ ∀ z ∈ y ∈ B | C ∈ A ∧ φ x = ⦋ z / y⦌ C ↔ ∀ y ∈ B C ∈ A ∧ φ → x = C
49 48 eubii ⊢ ∃! x ∀ z ∈ y ∈ B | C ∈ A ∧ φ x = ⦋ z / y⦌ C ↔ ∃! x ∀ y ∈ B C ∈ A ∧ φ → x = C
50 34 49 bitri ⊢ ∃! x ∃ z ∈ y ∈ B | C ∈ A ∧ φ x = ⦋ z / y⦌ C ↔ ∃! x ∀ y ∈ B C ∈ A ∧ φ → x = C
51 1 23 50 3bitri ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ x = C ↔ ∃! x ∀ y ∈ B C ∈ A ∧ φ → x = C