Theorem bj-brrelex12ALT

Description: Two classes related by a binary relation are both sets. Alternate proof of brrelex12 . (Contributed by BJ, 14-Jul-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-brrelex12ALT	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		0nelrel0	⊢ ( Rel 𝑅 → ¬ ∅ ∈ 𝑅 )
2		jcn	⊢ ( 𝐴 𝑅 𝐵 → ( ¬ ∅ ∈ 𝑅 → ¬ ( 𝐴 𝑅 𝐵 → ∅ ∈ 𝑅 ) ) )
3	2	impcom	⊢ ( ( ¬ ∅ ∈ 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ¬ ( 𝐴 𝑅 𝐵 → ∅ ∈ 𝑅 ) )
4		opprc	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
5		df-br	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
6	5	biimpi	⊢ ( 𝐴 𝑅 𝐵 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
7		eleq1	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ∅ → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ∅ ∈ 𝑅 ) )
8	6 7	imbitrid	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ∅ → ( 𝐴 𝑅 𝐵 → ∅ ∈ 𝑅 ) )
9	4 8	syl	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 𝑅 𝐵 → ∅ ∈ 𝑅 ) )
10	3 9	nsyl2	⊢ ( ( ¬ ∅ ∈ 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
11	1 10	sylan	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )