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 ω N ω I ω J ω I 𝑔 J = M 𝑔 N I = M J = N

Proof

Step Hyp Ref Expression
1 goel I ω J ω I 𝑔 J = I J
2 goel M ω N ω M 𝑔 N = M N
3 1 2 eqeqan12rd M ω N ω I ω J ω I 𝑔 J = M 𝑔 N I J = M N
4 0ex V
5 opex I J 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 ω J ω I J = M N I = M J = N
10 9 adantl M ω N ω I ω J ω I J = M N I = M J = N
11 8 10 bitr3id M ω N ω I ω J ω = I J = M N I = M J = N
12 6 11 syl5bb M ω N ω I ω J ω I J = M N I = M J = N
13 3 12 bitrd M ω N ω I ω J ω I 𝑔 J = M 𝑔 N I = M J = N