Metamath Proof Explorer

Theorem goeleq12bg

Description: Two "Godel-set of membership" codes for two variables are equal iff the two corresponding variables are equal. (Contributed by AV, 8-Oct-2023)

Ref Expression
Assertion goeleq12bg 
|- ( ( ( M e. _om /\ N e. _om ) /\ ( I e. _om /\ J e. _om ) ) -> ( ( I e.g J ) = ( M e.g N ) <-> ( I = M /\ J = N ) ) )

Proof

Step Hyp Ref Expression
1 goel 
 |-  ( ( I e. _om /\ J e. _om ) -> ( I e.g J ) = <. (/) , <. I , J >. >. )
2 goel 
 |-  ( ( M e. _om /\ N e. _om ) -> ( M e.g N ) = <. (/) , <. M , N >. >. )
3 1 2 eqeqan12rd 
 |-  ( ( ( M e. _om /\ N e. _om ) /\ ( I e. _om /\ J e. _om ) ) -> ( ( I e.g J ) = ( M e.g N ) <-> <. (/) , <. I , J >. >. = <. (/) , <. M , N >. >. ) )
4 0ex 
 |-  (/) e. _V
5 opex 
 |-  <. I , J >. e. _V
6 4 5 opth 
 |-  ( <. (/) , <. I , J >. >. = <. (/) , <. M , N >. >. <-> ( (/) = (/) /\ <. I , J >. = <. M , N >. ) )
7 eqid 
 |-  (/) = (/)
8 7 biantrur 
 |-  ( <. I , J >. = <. M , N >. <-> ( (/) = (/) /\ <. I , J >. = <. M , N >. ) )
9 opthg 
 |-  ( ( I e. _om /\ J e. _om ) -> ( <. I , J >. = <. M , N >. <-> ( I = M /\ J = N ) ) )
10 9 adantl 
 |-  ( ( ( M e. _om /\ N e. _om ) /\ ( I e. _om /\ J e. _om ) ) -> ( <. I , J >. = <. M , N >. <-> ( I = M /\ J = N ) ) )
11 8 10 bitr3id 
 |-  ( ( ( M e. _om /\ N e. _om ) /\ ( I e. _om /\ J e. _om ) ) -> ( ( (/) = (/) /\ <. I , J >. = <. M , N >. ) <-> ( I = M /\ J = N ) ) )
12 6 11 syl5bb 
 |-  ( ( ( M e. _om /\ N e. _om ) /\ ( I e. _om /\ J e. _om ) ) -> ( <. (/) , <. I , J >. >. = <. (/) , <. M , N >. >. <-> ( I = M /\ J = N ) ) )
13 3 12 bitrd 
 |-  ( ( ( M e. _om /\ N e. _om ) /\ ( I e. _om /\ J e. _om ) ) -> ( ( I e.g J ) = ( M e.g N ) <-> ( I = M /\ J = N ) ) )