Description: Domain membership. Theorem 4 of Suppes p. 59. (Contributed by Mario Carneiro, 9-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | eldmg | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom 𝐵 ↔ ∃ 𝑦 𝐴 𝐵 𝑦 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 | ⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝐵 𝑦 ↔ 𝑤 𝐵 𝑦 ) ) | |
2 | 1 | exbidv | ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 𝑥 𝐵 𝑦 ↔ ∃ 𝑦 𝑤 𝐵 𝑦 ) ) |
3 | breq1 | ⊢ ( 𝑤 = 𝐴 → ( 𝑤 𝐵 𝑦 ↔ 𝐴 𝐵 𝑦 ) ) | |
4 | 3 | exbidv | ⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑦 𝑤 𝐵 𝑦 ↔ ∃ 𝑦 𝐴 𝐵 𝑦 ) ) |
5 | df-dm | ⊢ dom 𝐵 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐵 𝑦 } | |
6 | 2 4 5 | elab2gw | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom 𝐵 ↔ ∃ 𝑦 𝐴 𝐵 𝑦 ) ) |