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

Metamath Proof Explorer

Theorem notabw

Description: A class abstraction defined by a negation. Version of notab using implicit substitution, which does not require ax-10 , ax-12 . (Contributed by GG, 15-Oct-2024)

		Ref	Expression
	Hypothesis	notabw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	Assertion	notabw	⊢ { 𝑥 ∣ ¬ 𝜑 } = ( V ∖ { 𝑦 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		notabw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		vex	⊢ 𝑥 ∈ V
3	2	biantrur	⊢ ( ¬ 𝑥 ∈ { 𝑦 ∣ 𝜓 } ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝜓 } ) )
4		df-clab	⊢ ( 𝑥 ∈ { 𝑦 ∣ 𝜓 } ↔ [ 𝑥 / 𝑦 ] 𝜓 )
5	1	bicomd	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜑 ) )
6	5	equcoms	⊢ ( 𝑦 = 𝑥 → ( 𝜓 ↔ 𝜑 ) )
7	6	sbievw	⊢ ( [ 𝑥 / 𝑦 ] 𝜓 ↔ 𝜑 )
8	4 7	bitri	⊢ ( 𝑥 ∈ { 𝑦 ∣ 𝜓 } ↔ 𝜑 )
9	3 8	xchnxbi	⊢ ( ¬ 𝜑 ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝜓 } ) )
10	9	abbii	⊢ { 𝑥 ∣ ¬ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝜓 } ) }
11		df-dif	⊢ ( V ∖ { 𝑦 ∣ 𝜓 } ) = { 𝑥 ∣ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝜓 } ) }
12	10 11	eqtr4i	⊢ { 𝑥 ∣ ¬ 𝜑 } = ( V ∖ { 𝑦 ∣ 𝜓 } )