Theorem opelvvdif

Description: Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019)

	Ref	Expression
Assertion	opelvvdif	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( V × V ) ∖ 𝑅 ) ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( V × V ) ∖ 𝑅 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) )
2		opelvvg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )
3	2	biantrurd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) ) )
4	1 3	bitr4id	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( V × V ) ∖ 𝑅 ) ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) )