Metamath Proof Explorer

Theorem emptynf

Description: On the empty domain, any variable is effectively nonfree in any formula. (Contributed by Wolf Lammen, 12-Mar-2023)

Ref Expression
Assertion emptynf 
|- ( -. E. x T. -> F/ x ph )

Proof

Step Hyp Ref Expression
1 emptyal 
 |-  ( -. E. x T. -> A. x ph )
2 nftht 
 |-  ( A. x ph -> F/ x ph )
3 1 2 syl 
 |-  ( -. E. x T. -> F/ x ph )