Metamath Proof Explorer


Theorem notab

Description: A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010)

Ref Expression
Assertion notab x|¬φ=Vx|φ

Proof

Step Hyp Ref Expression
1 df-rab xV|¬φ=x|xV¬φ
2 rabab xV|¬φ=x|¬φ
3 1 2 eqtr3i x|xV¬φ=x|¬φ
4 difab x|xVx|φ=x|xV¬φ
5 abid2 x|xV=V
6 5 difeq1i x|xVx|φ=Vx|φ
7 4 6 eqtr3i x|xV¬φ=Vx|φ
8 3 7 eqtr3i x|¬φ=Vx|φ