Theorem relbrcnvg

Description: When R is a relation, the sethood assumptions on brcnv can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	relbrcnvg	⊢ ( Rel 𝑅 → ( 𝐴 ◡ 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ 𝑅
2	1	brrelex12i	⊢ ( 𝐴 ◡ 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
3	2	a1i	⊢ ( Rel 𝑅 → ( 𝐴 ◡ 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
4		brrelex12	⊢ ( ( Rel 𝑅 ∧ 𝐵 𝑅 𝐴 ) → ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) )
5	4	ancomd	⊢ ( ( Rel 𝑅 ∧ 𝐵 𝑅 𝐴 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
6	5	ex	⊢ ( Rel 𝑅 → ( 𝐵 𝑅 𝐴 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
7		brcnvg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ◡ 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )
8	7	a1i	⊢ ( Rel 𝑅 → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ◡ 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) ) )
9	3 6 8	pm5.21ndd	⊢ ( Rel 𝑅 → ( 𝐴 ◡ 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )