Metamath Proof Explorer

Theorem rext0

Description: Nonempty existential quantification of a theorem is true. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Hypothesis rext0.1 
|- ph
Assertion rext0 
|- ( E. x e. A ph <-> A =/= (/) )

Proof

Step Hyp Ref Expression
1 rext0.1 
 |-  ph
2 1 notnoti 
 |-  -. -. ph
3 2 ralf0 
 |-  ( A. x e. A -. ph <-> A = (/) )
4 3 notbii 
 |-  ( -. A. x e. A -. ph <-> -. A = (/) )
5 dfrex2 
 |-  ( E. x e. A ph <-> -. A. x e. A -. ph )
6 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
7 4 5 6 3bitr4i 
 |-  ( E. x e. A ph <-> A =/= (/) )