This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem notzfaus

Description: In the Separation Scheme zfauscl , we require that y not occur in ph (which can be generalized to "not be free in"). Here we show special cases of A and ph that result in a contradiction if that requirement is not met. (Contributed by NM, 8-Feb-2006) (Proof shortened by BJ, 18-Nov-2023)

Ref Expression
Hypotheses notzfaus.1 
|- A = { (/) }
notzfaus.2 
|- ( ph <-> -. x e. y )
Assertion notzfaus 
|- -. E. y A. x ( x e. y <-> ( x e. A /\ ph ) )

Proof

Step Hyp Ref Expression
1 notzfaus.1 
 |-  A = { (/) }
2 notzfaus.2 
 |-  ( ph <-> -. x e. y )
3 0ex 
 |-  (/) e. _V
4 3 snnz 
 |-  { (/) } =/= (/)
5 1 4 eqnetri 
 |-  A =/= (/)
6 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
7 5 6 mpbi 
 |-  E. x x e. A
8 pm5.19 
 |-  -. ( x e. y <-> -. x e. y )
9 ibar 
 |-  ( x e. A -> ( ph <-> ( x e. A /\ ph ) ) )
10 9 2 bitr3di 
 |-  ( x e. A -> ( ( x e. A /\ ph ) <-> -. x e. y ) )
11 10 bibi2d 
 |-  ( x e. A -> ( ( x e. y <-> ( x e. A /\ ph ) ) <-> ( x e. y <-> -. x e. y ) ) )
12 8 11 mtbiri 
 |-  ( x e. A -> -. ( x e. y <-> ( x e. A /\ ph ) ) )
13 7 12 eximii 
 |-  E. x -. ( x e. y <-> ( x e. A /\ ph ) )
14 exnal 
 |-  ( E. x -. ( x e. y <-> ( x e. A /\ ph ) ) <-> -. A. x ( x e. y <-> ( x e. A /\ ph ) ) )
15 13 14 mpbi 
 |-  -. A. x ( x e. y <-> ( x e. A /\ ph ) )
16 15 nex 
 |-  -. E. y A. x ( x e. y <-> ( x e. A /\ ph ) )