Description: Nonemptiness is absolute for transitive models. Compare Example I.16.3 of Kunen2 p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | n0abso | |- ( ( Tr M /\ A e. M ) -> ( A =/= (/) <-> E. x e. M x e. A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rexabso | |- ( ( Tr M /\ A e. M ) -> ( E. x e. A T. <-> E. x e. M ( x e. A /\ T. ) ) ) |
|
| 2 | tru | |- T. |
|
| 3 | 2 | rext0 | |- ( E. x e. A T. <-> A =/= (/) ) |
| 4 | 3 | bicomi | |- ( A =/= (/) <-> E. x e. A T. ) |
| 5 | 2 | biantru | |- ( x e. A <-> ( x e. A /\ T. ) ) |
| 6 | 5 | rexbii | |- ( E. x e. M x e. A <-> E. x e. M ( x e. A /\ T. ) ) |
| 7 | 1 4 6 | 3bitr4g | |- ( ( Tr M /\ A e. M ) -> ( A =/= (/) <-> E. x e. M x e. A ) ) |