Theorem bj-ideqgALT

Description: Alternate proof of bj-ideqg from brabga instead of bj-opelid itself proved from bj-opelidb . (Contributed by BJ, 27-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-ideqgALT	$$⊢A\cap B\in V\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
2	1	brrelex12i	$$⊢A\mathrm{I}B\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
3	2	adantl	$$⊢\left(A\cap B\in V\wedge A\mathrm{I}B\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
4		bj-inexeqex	$$⊢\left(A\cap B\in V\wedge A=B\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
5		eqeq12	$$⊢\left(x=A\wedge y=B\right)\to \left(x=y\leftrightarrow A=B\right)$$
6		df-id	$$⊢\mathrm{I}=\left\{⟨x,y⟩|x=y\right\}$$
7	5 6	brabga	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$
8	3 4 7	pm5.21nd	$$⊢A\cap B\in V\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$