Metamath Proof Explorer


Theorem prv

Description: The "proves" relation on a set. A wff encoded as U is true in a model M iff for every valuation s e. ( M ^m _om ) , the interpretation of the wff using the membership relation on M is true. (Contributed by AV, 5-Nov-2023)

Ref Expression
Assertion prv M V U W M U M Sat U = M ω

Proof

Step Hyp Ref Expression
1 oveq12 m = M u = U m Sat u = M Sat U
2 simpl m = M u = U m = M
3 2 oveq1d m = M u = U m ω = M ω
4 1 3 eqeq12d m = M u = U m Sat u = m ω M Sat U = M ω
5 df-prv = m u | m Sat u = m ω
6 4 5 brabga M V U W M U M Sat U = M ω