Theorem: LO.FirstOrder.Structure.mem_theory_iff (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
σ : Sentence L
⊢ σ ∈ theory L M ↔ M ⊧ₘ σ
Tactic:
rfl
State after:
no goals