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 φ¬xy
Assertion notzfaus ¬yxxyxAφ

Proof

Step Hyp Ref Expression
1 notzfaus.1 A=
2 notzfaus.2 φ¬xy
3 0ex V
4 3 snnz
5 1 4 eqnetri A
6 n0 AxxA
7 5 6 mpbi xxA
8 pm5.19 ¬xy¬xy
9 ibar xAφxAφ
10 9 2 bitr3di xAxAφ¬xy
11 10 bibi2d xAxyxAφxy¬xy
12 8 11 mtbiri xA¬xyxAφ
13 7 12 eximii x¬xyxAφ
14 exnal x¬xyxAφ¬xxyxAφ
15 13 14 mpbi ¬xxyxAφ
16 15 nex ¬yxxyxAφ