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 i^i B ) e. V -> ( A _I B <-> A = B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reli | |- Rel _I |
|
| 2 | 1 | brrelex12i | |- ( A _I B -> ( A e. _V /\ B e. _V ) ) |
| 3 | 2 | adantl | |- ( ( ( A i^i B ) e. V /\ A _I B ) -> ( A e. _V /\ B e. _V ) ) |
| 4 | bj-inexeqex | |- ( ( ( A i^i B ) e. V /\ A = B ) -> ( A e. _V /\ B e. _V ) ) |
|
| 5 | eqeq12 | |- ( ( x = A /\ y = B ) -> ( x = y <-> A = B ) ) |
|
| 6 | df-id | |- _I = { <. x , y >. | x = y } |
|
| 7 | 5 6 | brabga | |- ( ( A e. _V /\ B e. _V ) -> ( A _I B <-> A = B ) ) |
| 8 | 3 4 7 | pm5.21nd | |- ( ( A i^i B ) e. V -> ( A _I B <-> A = B ) ) |