simp [memRelOpr, pair_defined.df.iff, memRel_defined.df.iff]
ξ : Type u_1
n : ?m.134755
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y r : M
⊢ (Semiformula.Eval (standardModel M) ![r, x, y] Empty.elim) memRelOpr.sentence ↔ ⟪x, y⟫ ∈ r
no goals