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

Metamath Proof Explorer

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 ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝜑 }