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 | ||
Assertion | sategoelfv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sategoelfvb.s | ||
2 | 1 | sategoelfvb | |
3 | simpr | ||
4 | 2 3 | syl6bi | |
5 | 4 | 3impia |