Metamath Proof Explorer


Theorem sate0fv0

Description: A simplified satisfaction predicate as function over wff codes over an empty model is an empty set. (Contributed by AV, 31-Oct-2023)

Ref Expression
Assertion sate0fv0 U Fmla ω S Sat U S =

Proof

Step Hyp Ref Expression
1 0ex V
2 satef V U Fmla ω S Sat U S : ω
3 1 2 mp3an1 U Fmla ω S Sat U S : ω
4 3 ex U Fmla ω S Sat U S : ω
5 f00 S : ω S = ω =
6 5 simplbi S : ω S =
7 4 6 syl6 U Fmla ω S Sat U S =