Theorem vvdifopab

Description: Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019)

	Ref	Expression
Assertion	vvdifopab	⊢ ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
2	1	notbii	⊢ ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ¬ 𝜑 )
3		opelvvdif	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) ↔ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
4	3	el2v	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) ↔ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
5		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 } ↔ ¬ 𝜑 )
6	2 4 5	3bitr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 } )
7	6	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 } )
8		relxp	⊢ Rel ( V × V )
9		reldif	⊢ ( Rel ( V × V ) → Rel ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
10	8 9	ax-mp	⊢ Rel ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
11		relopabv	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 }
12		nfcv	⊢ Ⅎ 𝑥 ( V × V )
13		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
14	12 13	nfdif	⊢ Ⅎ 𝑥 ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
15		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 }
16		nfcv	⊢ Ⅎ 𝑦 ( V × V )
17		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
18	16 17	nfdif	⊢ Ⅎ 𝑦 ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
19		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 }
20	14 15 18 19	eqrelf	⊢ ( ( Rel ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) ∧ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 } ) → ( ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 } ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 } ) ) )
21	10 11 20	mp2an	⊢ ( ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 } ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 } ) )
22	7 21	mpbir	⊢ ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 }