Theorem dfnelbr2

Description: Alternate definition of the negated membership as binary relation. (Proposed by BJ, 27-Dec-2021.) (Contributed by AV, 27-Dec-2021)

	Ref	Expression
Assertion	dfnelbr2	⊢ _∉ = ( ( V × V ) ∖ E )

Proof

Step	Hyp	Ref	Expression
1		difopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ ¬ 𝑥 ∈ 𝑦 ) }
2		df-xp	⊢ ( V × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
3		df-eprel	⊢ E = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 }
4	2 3	difeq12i	⊢ ( ( V × V ) ∖ E ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 } )
5		df-nelbr	⊢ _∉ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝑥 ∈ 𝑦 }
6		vex	⊢ 𝑥 ∈ V
7		vex	⊢ 𝑦 ∈ V
8	6 7	pm3.2i	⊢ ( 𝑥 ∈ V ∧ 𝑦 ∈ V )
9	8	biantrur	⊢ ( ¬ 𝑥 ∈ 𝑦 ↔ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ ¬ 𝑥 ∈ 𝑦 ) )
10	9	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝑥 ∈ 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ ¬ 𝑥 ∈ 𝑦 ) }
11	5 10	eqtri	⊢ _∉ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ ¬ 𝑥 ∈ 𝑦 ) }
12	1 4 11	3eqtr4ri	⊢ _∉ = ( ( V × V ) ∖ E )