Description: The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel and closed form of epeli . (Contributed by Scott Fenton, 27-Mar-2011) (Revised by Mario Carneiro, 28-Apr-2015) TODO: move it to the main section after reordering to have brrelex1i available. (Proof shortened by BJ, 14-Jul-2023) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-epelg | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rele | ⊢ Rel E | |
| 2 | 1 | brrelex1i | ⊢ ( 𝐴 E 𝐵 → 𝐴 ∈ V ) |
| 3 | 2 | a1i | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 E 𝐵 → 𝐴 ∈ V ) ) |
| 4 | elex | ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V ) | |
| 5 | 4 | a1i | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V ) ) |
| 6 | eleq12 | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 ∈ 𝑦 ↔ 𝐴 ∈ 𝐵 ) ) | |
| 7 | df-eprel | ⊢ E = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 } | |
| 8 | 6 7 | brabga | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) ) |
| 9 | 8 | expcom | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ V → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) ) ) |
| 10 | 3 5 9 | pm5.21ndd | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) ) |