Theorem elcnv2

Description: Membership in a converse relation. Equation 5 of Suppes p. 62. (Contributed by NM, 11-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		elcnv	⊢ ( 𝐴 ∈ ◡ 𝑅 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 𝑅 𝑥 ) )
2		df-br	⊢ ( 𝑦 𝑅 𝑥 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 )
3	2	anbi2i	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
4	3	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 𝑅 𝑥 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
5	1 4	bitri	⊢ ( 𝐴 ∈ ◡ 𝑅 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )