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 𝐵 ↔ 𝐴 ∈ 𝐵 ) )