Metamath Proof Explorer

Theorem fmlan0

Description: The empty set is not a Godel formula. (Contributed by AV, 19-Nov-2023)

Ref Expression
Assertion fmlan0 
|- (/) e/ ( Fmla ` _om )

Proof

Step Hyp Ref Expression
1 fmlaomn0 
 |-  ( x e. _om -> (/) e/ ( Fmla ` x ) )
2 df-nel 
 |-  ( (/) e/ ( Fmla ` x ) <-> -. (/) e. ( Fmla ` x ) )
3 1 2 sylib 
 |-  ( x e. _om -> -. (/) e. ( Fmla ` x ) )
4 3 nrex 
 |-  -. E. x e. _om (/) e. ( Fmla ` x )
5 df-nel 
 |-  ( (/) e/ ( Fmla ` _om ) <-> -. (/) e. ( Fmla ` _om ) )
6 fmla 
 |-  ( Fmla ` _om ) = U_ x e. _om ( Fmla ` x )
7 6 eleq2i 
 |-  ( (/) e. ( Fmla ` _om ) <-> (/) e. U_ x e. _om ( Fmla ` x ) )
8 eliun 
 |-  ( (/) e. U_ x e. _om ( Fmla ` x ) <-> E. x e. _om (/) e. ( Fmla ` x ) )
9 7 8 bitri 
 |-  ( (/) e. ( Fmla ` _om ) <-> E. x e. _om (/) e. ( Fmla ` x ) )
10 5 9 xchbinx 
 |-  ( (/) e/ ( Fmla ` _om ) <-> -. E. x e. _om (/) e. ( Fmla ` x ) )
11 4 10 mpbir 
 |-  (/) e/ ( Fmla ` _om )