Metamath Proof Explorer

Theorem eldm3

Description: Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017)

Ref Expression
Assertion eldm3 ⊢ A ∈ dom ⁡ B ↔ B ↾ A ≠ ∅

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ dom ⁡ B → A ∈ V
2 snprc ⊢ ¬ A ∈ V ↔ A = ∅
3 reseq2 ⊢ A = ∅ → B ↾ A = B ↾ ∅
4 res0 ⊢ B ↾ ∅ = ∅
5 3 4 eqtrdi ⊢ A = ∅ → B ↾ A = ∅
6 2 5 sylbi ⊢ ¬ A ∈ V → B ↾ A = ∅
7 6 necon1ai ⊢ B ↾ A ≠ ∅ → A ∈ V
8 eleq1 ⊢ x = A → x ∈ dom ⁡ B ↔ A ∈ dom ⁡ B
9 sneq ⊢ x = A → x = A
10 9 reseq2d ⊢ x = A → B ↾ x = B ↾ A
11 10 neeq1d ⊢ x = A → B ↾ x ≠ ∅ ↔ B ↾ A ≠ ∅
12 dfclel ⊢ x y ∈ B ↔ ∃ p p = x y ∧ p ∈ B
13 12 exbii ⊢ ∃ y x y ∈ B ↔ ∃ y ∃ p p = x y ∧ p ∈ B
14 vex ⊢ x ∈ V
15 14 eldm2 ⊢ x ∈ dom ⁡ B ↔ ∃ y x y ∈ B
16 n0 ⊢ B ↾ x ≠ ∅ ↔ ∃ p p ∈ B ↾ x
17 elres ⊢ p ∈ B ↾ x ↔ ∃ z ∈ x ∃ y p = z y ∧ z y ∈ B
18 eleq1 ⊢ p = z y → p ∈ B ↔ z y ∈ B
19 18 pm5.32i ⊢ p = z y ∧ p ∈ B ↔ p = z y ∧ z y ∈ B
20 opeq1 ⊢ z = x → z y = x y
21 20 eqeq2d ⊢ z = x → p = z y ↔ p = x y
22 21 anbi1d ⊢ z = x → p = z y ∧ p ∈ B ↔ p = x y ∧ p ∈ B
23 19 22 bitr3id ⊢ z = x → p = z y ∧ z y ∈ B ↔ p = x y ∧ p ∈ B
24 23 exbidv ⊢ z = x → ∃ y p = z y ∧ z y ∈ B ↔ ∃ y p = x y ∧ p ∈ B
25 14 24 rexsn ⊢ ∃ z ∈ x ∃ y p = z y ∧ z y ∈ B ↔ ∃ y p = x y ∧ p ∈ B
26 17 25 bitri ⊢ p ∈ B ↾ x ↔ ∃ y p = x y ∧ p ∈ B
27 26 exbii ⊢ ∃ p p ∈ B ↾ x ↔ ∃ p ∃ y p = x y ∧ p ∈ B
28 excom ⊢ ∃ p ∃ y p = x y ∧ p ∈ B ↔ ∃ y ∃ p p = x y ∧ p ∈ B
29 16 27 28 3bitri ⊢ B ↾ x ≠ ∅ ↔ ∃ y ∃ p p = x y ∧ p ∈ B
30 13 15 29 3bitr4i ⊢ x ∈ dom ⁡ B ↔ B ↾ x ≠ ∅
31 8 11 30 vtoclbg ⊢ A ∈ V → A ∈ dom ⁡ B ↔ B ↾ A ≠ ∅
32 1 7 31 pm5.21nii ⊢ A ∈ dom ⁡ B ↔ B ↾ A ≠ ∅