Metamath Proof Explorer


Theorem sategoelfv

Description: Condition of a valuation S of a simplified satisfaction predicate for a Godel-set of membership: The sets in model M corresponding to the variables A and B under the assignment of S are in a membership relation in M . (Contributed by AV, 5-Nov-2023)

Ref Expression
Hypothesis sategoelfvb.s E = M Sat A 𝑔 B
Assertion sategoelfv M V A ω B ω S E S A S B

Proof

Step Hyp Ref Expression
1 sategoelfvb.s E = M Sat A 𝑔 B
2 1 sategoelfvb M V A ω B ω S E S M ω S A S B
3 simpr S M ω S A S B S A S B
4 2 3 syl6bi M V A ω B ω S E S A S B
5 4 3impia M V A ω B ω S E S A S B