Theorem compab

Description: Two ways of saying "the complement of a class abstraction". (Contributed by Andrew Salmon, 15-Jul-2011) (Proof shortened by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Assertion	compab	⊢ ( V ∖ { 𝑧 ∣ 𝜑 } ) = { 𝑧 ∣ ¬ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑧 V
2		nfab1	⊢ Ⅎ 𝑧 { 𝑧 ∣ 𝜑 }
3	1 2	nfdif	⊢ Ⅎ 𝑧 ( V ∖ { 𝑧 ∣ 𝜑 } )
4		nfab1	⊢ Ⅎ 𝑧 { 𝑧 ∣ ¬ 𝜑 }
5	3 4	cleqf	⊢ ( ( V ∖ { 𝑧 ∣ 𝜑 } ) = { 𝑧 ∣ ¬ 𝜑 } ↔ ∀ 𝑧 ( 𝑧 ∈ ( V ∖ { 𝑧 ∣ 𝜑 } ) ↔ 𝑧 ∈ { 𝑧 ∣ ¬ 𝜑 } ) )
6		abid	⊢ ( 𝑧 ∈ { 𝑧 ∣ 𝜑 } ↔ 𝜑 )
7	6	notbii	⊢ ( ¬ 𝑧 ∈ { 𝑧 ∣ 𝜑 } ↔ ¬ 𝜑 )
8		velcomp	⊢ ( 𝑧 ∈ ( V ∖ { 𝑧 ∣ 𝜑 } ) ↔ ¬ 𝑧 ∈ { 𝑧 ∣ 𝜑 } )
9		abid	⊢ ( 𝑧 ∈ { 𝑧 ∣ ¬ 𝜑 } ↔ ¬ 𝜑 )
10	7 8 9	3bitr4i	⊢ ( 𝑧 ∈ ( V ∖ { 𝑧 ∣ 𝜑 } ) ↔ 𝑧 ∈ { 𝑧 ∣ ¬ 𝜑 } )
11	5 10	mpgbir	⊢ ( V ∖ { 𝑧 ∣ 𝜑 } ) = { 𝑧 ∣ ¬ 𝜑 }