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 \in ω \land N \in ω) \land (I \in ω \land J \in ω)) \to (I \in_{𝑔} J = M \in_{𝑔} N \leftrightarrow (I = M \land J = N))$

Proof

Step	Hyp	Ref	Expression
1		goel	$⊢ (I \in ω \land J \in ω) \to I \in_{𝑔} J = ⟨\emptyset, ⟨I, J⟩⟩$
2		goel	$⊢ (M \in ω \land N \in ω) \to M \in_{𝑔} N = ⟨\emptyset, ⟨M, N⟩⟩$
3	1 2	eqeqan12rd	$⊢ ((M \in ω \land N \in ω) \land (I \in ω \land J \in ω)) \to (I \in_{𝑔} J = M \in_{𝑔} N \leftrightarrow ⟨\emptyset, ⟨I, J⟩⟩ = ⟨\emptyset, ⟨M, N⟩⟩)$
4		0ex	$⊢ \emptyset \in V$
5		opex	$⊢ ⟨I, J⟩ \in V$
6	4 5	opth	$⊢ ⟨\emptyset, ⟨I, J⟩⟩ = ⟨\emptyset, ⟨M, N⟩⟩ \leftrightarrow (\emptyset = \emptyset \land ⟨I, J⟩ = ⟨M, N⟩)$
7		eqid	$⊢ \emptyset = \emptyset$
8	7	biantrur	$⊢ ⟨I, J⟩ = ⟨M, N⟩ \leftrightarrow (\emptyset = \emptyset \land ⟨I, J⟩ = ⟨M, N⟩)$
9		opthg	$⊢ (I \in ω \land J \in ω) \to (⟨I, J⟩ = ⟨M, N⟩ \leftrightarrow (I = M \land J = N))$
10	9	adantl	$⊢ ((M \in ω \land N \in ω) \land (I \in ω \land J \in ω)) \to (⟨I, J⟩ = ⟨M, N⟩ \leftrightarrow (I = M \land J = N))$
11	8 10	bitr3id	$⊢ ((M \in ω \land N \in ω) \land (I \in ω \land J \in ω)) \to ((\emptyset = \emptyset \land ⟨I, J⟩ = ⟨M, N⟩) \leftrightarrow (I = M \land J = N))$
12	6 11	syl5bb	$⊢ ((M \in ω \land N \in ω) \land (I \in ω \land J \in ω)) \to (⟨\emptyset, ⟨I, J⟩⟩ = ⟨\emptyset, ⟨M, N⟩⟩ \leftrightarrow (I = M \land J = N))$
13	3 12	bitrd	$⊢ ((M \in ω \land N \in ω) \land (I \in ω \land J \in ω)) \to (I \in_{𝑔} J = M \in_{𝑔} N \leftrightarrow (I = M \land J = N))$