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	⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ( 𝐼 ∈𝑔 𝐽 ) = ( 𝑀 ∈𝑔 𝑁 ) ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		goel	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ∈𝑔 𝐽 ) = ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ )
2		goel	⊢ ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) → ( 𝑀 ∈𝑔 𝑁 ) = ⟨ ∅ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
3	1 2	eqeqan12rd	⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ( 𝐼 ∈𝑔 𝐽 ) = ( 𝑀 ∈𝑔 𝑁 ) ↔ ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) )
4		0ex	⊢ ∅ ∈ V
5		opex	⊢ ⟨ 𝐼 , 𝐽 ⟩ ∈ V
6	4 5	opth	⊢ ( ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ↔ ( ∅ = ∅ ∧ ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ) )
7		eqid	⊢ ∅ = ∅
8	7	biantrur	⊢ ( ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ∅ = ∅ ∧ ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ) )
9		opthg	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )
10	9	adantl	⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )
11	8 10	bitr3id	⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ( ∅ = ∅ ∧ ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )
12	6 11	syl5bb	⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )
13	3 12	bitrd	⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ( 𝐼 ∈𝑔 𝐽 ) = ( 𝑀 ∈𝑔 𝑁 ) ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )