**Description:** Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004)

Ref | Expression | ||
---|---|---|---|

Assertion | 0el | ⊢ ( ∅ ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | risset | ⊢ ( ∅ ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = ∅ ) | |

2 | eq0 | ⊢ ( 𝑥 = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) | |

3 | 2 | rexbii | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) |

4 | 1 3 | bitri | ⊢ ( ∅ ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) |