Metamath Proof Explorer

Theorem difopab

Description: Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion difopab ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ ¬ 𝜓 ) }

Proof

Step Hyp Ref Expression
1 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2 reldif ⊢ ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → Rel ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
3 1 2 ax-mp ⊢ Rel ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
4 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ ¬ 𝜓 ) }
5 sbcan ⊢ ( [ 𝑧 / 𝑥 ] ( [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] ¬ 𝜓 ) ↔ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ¬ 𝜓 ) )
6 sbcan ⊢ ( [ 𝑤 / 𝑦 ] ( 𝜑 ∧ ¬ 𝜓 ) ↔ ( [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] ¬ 𝜓 ) )
7 6 sbcbii ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ( 𝜑 ∧ ¬ 𝜓 ) ↔ [ 𝑧 / 𝑥 ] ( [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] ¬ 𝜓 ) )
8 opelopabsb ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
9 sbcng ⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑥 ] ¬ [ 𝑤 / 𝑦 ] 𝜓 ↔ ¬ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 ) )
10 9 elv ⊢ ( [ 𝑧 / 𝑥 ] ¬ [ 𝑤 / 𝑦 ] 𝜓 ↔ ¬ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 )
11 sbcng ⊢ ( 𝑤 ∈ V → ( [ 𝑤 / 𝑦 ] ¬ 𝜓 ↔ ¬ [ 𝑤 / 𝑦 ] 𝜓 ) )
12 11 elv ⊢ ( [ 𝑤 / 𝑦 ] ¬ 𝜓 ↔ ¬ [ 𝑤 / 𝑦 ] 𝜓 )
13 12 sbcbii ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ¬ 𝜓 ↔ [ 𝑧 / 𝑥 ] ¬ [ 𝑤 / 𝑦 ] 𝜓 )
14 opelopabsb ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 )
15 14 notbii ⊢ ( ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ¬ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 )
16 10 13 15 3bitr4ri ⊢ ( ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ¬ 𝜓 )
17 8 16 anbi12i ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ¬ 𝜓 ) )
18 5 7 17 3bitr4ri ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ( 𝜑 ∧ ¬ 𝜓 ) )
19 eldif ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
20 opelopabsb ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ ¬ 𝜓 ) } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ( 𝜑 ∧ ¬ 𝜓 ) )
21 18 19 20 3bitr4i ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ ¬ 𝜓 ) } )
22 3 4 21 eqrelriiv ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ ¬ 𝜓 ) }