This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ 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