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 R /\ A R B ) -> ( A e. _V /\ B e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		0nelrel0	|- ( Rel R -> -. (/) e. R )
2		jcn	|- ( A R B -> ( -. (/) e. R -> -. ( A R B -> (/) e. R ) ) )
3	2	impcom	|- ( ( -. (/) e. R /\ A R B ) -> -. ( A R B -> (/) e. R ) )
4		opprc	|- ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) )
5		df-br	|- ( A R B <-> <. A , B >. e. R )
6	5	biimpi	|- ( A R B -> <. A , B >. e. R )
7		eleq1	|- ( <. A , B >. = (/) -> ( <. A , B >. e. R <-> (/) e. R ) )
8	6 7	imbitrid	|- ( <. A , B >. = (/) -> ( A R B -> (/) e. R ) )
9	4 8	syl	|- ( -. ( A e. _V /\ B e. _V ) -> ( A R B -> (/) e. R ) )
10	3 9	nsyl2	|- ( ( -. (/) e. R /\ A R B ) -> ( A e. _V /\ B e. _V ) )
11	1 10	sylan	|- ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) )