This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem epelg

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 . Definition 1.6 of Schloeder p. 1. (Contributed by Scott Fenton, 27-Mar-2011) (Revised by Mario Carneiro, 28-Apr-2015) (Proof shortened by BJ, 14-Jul-2023)

Ref Expression
Assertion epelg ( 𝐵 ∈ 𝑉 → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-br ⊢ ( 𝐴 E 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ E )
2 0nelopab ⊢ ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 }
3 df-eprel ⊢ E = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 }
4 3 eqcomi ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 } = E
5 4 eleq2i ⊢ ( ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 } ↔ ∅ ∈ E )
6 2 5 mtbi ⊢ ¬ ∅ ∈ E
7 eleq1 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ∅ → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ E ↔ ∅ ∈ E ) )
8 6 7 mtbiri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ∅ → ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ E )
9 8 con2i ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ E → ¬ ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
10 opprc1 ⊢ ( ¬ 𝐴 ∈ V → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
11 9 10 nsyl2 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ E → 𝐴 ∈ V )
12 1 11 sylbi ⊢ ( 𝐴 E 𝐵 → 𝐴 ∈ V )
13 12 a1i ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 E 𝐵 → 𝐴 ∈ V ) )
14 elex ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
15 14 a1i ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V ) )
16 eleq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 ∈ 𝑦 ↔ 𝐴 ∈ 𝐵 ) )
17 16 3 brabga ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
18 17 expcom ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ V → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) ) )
19 13 15 18 pm5.21ndd ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) )