Description: Substituting a class in the false truth constant results in the false truth constant. The analogous result with the true truth constant does not hold in general since substituting a proper class results in falsehood ( sbcex ), but holds for sets by sbcg . (Contributed by BJ, 11-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbcfal | |- ( [. A / x ]. F. <-> F. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbcex | |- ( [. A / x ]. F. -> A e. _V ) |
|
| 2 | falim | |- ( F. -> A e. _V ) |
|
| 3 | sbcg | |- ( A e. _V -> ( [. A / x ]. F. <-> F. ) ) |
|
| 4 | 1 2 3 | pm5.21nii | |- ( [. A / x ]. F. <-> F. ) |