letI : Structure L N := Structure.ofEquiv φ
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁴ : Nonempty M
inst✝³ : Nonempty M₁
inst✝² : Nonempty M₂
inst✝¹ : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
N : Type u_5
inst✝ : Nonempty N
φ : M ≃ N
σ : Sentence L
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁴ : Nonempty M
inst✝³ : Nonempty M₁
inst✝² : Nonempty M₂
inst✝¹ : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
N : Type u_5
inst✝ : Nonempty N
φ : M ≃ N
σ : Sentence L
this : Structure L N := Structure.ofEquiv φ
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ