Theorem bj-ideqg1ALT

Description: Alternate proof of bj-ideqg1 using brabga instead of the "unbounded" version bj-brab2a1 or brab2a . (Contributed by BJ, 25-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)

TODO: delete once bj-ideqg is in the main section.

	Ref	Expression
Assertion	bj-ideqg1ALT	|- ( ( A e. V \/ B e. W ) -> ( A _I B <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		reli	|- Rel _I
2	1	brrelex12i	|- ( A _I B -> ( A e. _V /\ B e. _V ) )
3	2	adantl	|- ( ( ( A e. V \/ B e. W ) /\ A _I B ) -> ( A e. _V /\ B e. _V ) )
4		elex	|- ( A e. V -> A e. _V )
5	4	adantr	|- ( ( A e. V /\ A = B ) -> A e. _V )
6		eleq1	|- ( A = B -> ( A e. W <-> B e. W ) )
7	6	biimparc	|- ( ( B e. W /\ A = B ) -> A e. W )
8	7	elexd	|- ( ( B e. W /\ A = B ) -> A e. _V )
9	5 8	jaoian	|- ( ( ( A e. V \/ B e. W ) /\ A = B ) -> A e. _V )
10		eleq1	|- ( A = B -> ( A e. V <-> B e. V ) )
11	10	biimpac	|- ( ( A e. V /\ A = B ) -> B e. V )
12	11	elexd	|- ( ( A e. V /\ A = B ) -> B e. _V )
13		elex	|- ( B e. W -> B e. _V )
14	13	adantr	|- ( ( B e. W /\ A = B ) -> B e. _V )
15	12 14	jaoian	|- ( ( ( A e. V \/ B e. W ) /\ A = B ) -> B e. _V )
16	9 15	jca	|- ( ( ( A e. V \/ B e. W ) /\ A = B ) -> ( A e. _V /\ B e. _V ) )
17		eqeq12	|- ( ( x = A /\ y = B ) -> ( x = y <-> A = B ) )
18		df-id	|- _I = { <. x , y >. | x = y }
19	17 18	brabga	|- ( ( A e. _V /\ B e. _V ) -> ( A _I B <-> A = B ) )
20	3 16 19	pm5.21nd	|- ( ( A e. V \/ B e. W ) -> ( A _I B <-> A = B ) )