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

Metamath Proof Explorer

Theorem nabbib

Description: Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019) (Proof shortened by Wolf Lammen, 25-Nov-2019) Definitial form. (Revised by Wolf Lammen, 5-Mar-2025)

Ref Expression
Assertion nabbib 
|- ( { x | ph } =/= { x | ps } <-> E. x ( ph <-> -. ps ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( { x | ph } =/= { x | ps } <-> -. { x | ph } = { x | ps } )
2 exnal 
 |-  ( E. x -. ( ph <-> ps ) <-> -. A. x ( ph <-> ps ) )
3 xor3 
 |-  ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) )
4 3 exbii 
 |-  ( E. x -. ( ph <-> ps ) <-> E. x ( ph <-> -. ps ) )
5 2 4 bitr3i 
 |-  ( -. A. x ( ph <-> ps ) <-> E. x ( ph <-> -. ps ) )
6 abbib 
 |-  ( { x | ph } = { x | ps } <-> A. x ( ph <-> ps ) )
7 5 6 xchnxbir 
 |-  ( -. { x | ph } = { x | ps } <-> E. x ( ph <-> -. ps ) )
8 1 7 bitri 
 |-  ( { x | ph } =/= { x | ps } <-> E. x ( ph <-> -. ps ) )