Theorem elcnv

Description: Membership in a converse relation. Equation 5 of Suppes p. 62. (Contributed by NM, 24-Mar-1998)

	Ref	Expression
Assertion	elcnv	⊢ ( 𝐴 ∈ ◡ 𝑅 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 𝑅 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		df-cnv	⊢ ◡ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝑅 𝑥 }
2	1	eleq2i	⊢ ( 𝐴 ∈ ◡ 𝑅 ↔ 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝑅 𝑥 } )
3		elopab	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝑅 𝑥 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 𝑅 𝑥 ) )
4	2 3	bitri	⊢ ( 𝐴 ∈ ◡ 𝑅 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 𝑅 𝑥 ) )