Theorem difopab

Description: Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015) (Proof shortened by SN, 19-Dec-2024)

	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		sban	⊢ ( [ 𝑧 / 𝑥 ] ( [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] ¬ 𝜓 ) ↔ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ¬ 𝜓 ) )
6		sban	⊢ ( [ 𝑤 / 𝑦 ] ( 𝜑 ∧ ¬ 𝜓 ) ↔ ( [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] ¬ 𝜓 ) )
7	6	sbbii	⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ( 𝜑 ∧ ¬ 𝜓 ) ↔ [ 𝑧 / 𝑥 ] ( [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] ¬ 𝜓 ) )
8		vopelopabsb	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
9		sbn	⊢ ( [ 𝑧 / 𝑥 ] ¬ [ 𝑤 / 𝑦 ] 𝜓 ↔ ¬ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 )
10		sbn	⊢ ( [ 𝑤 / 𝑦 ] ¬ 𝜓 ↔ ¬ [ 𝑤 / 𝑦 ] 𝜓 )
11	10	sbbii	⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ¬ 𝜓 ↔ [ 𝑧 / 𝑥 ] ¬ [ 𝑤 / 𝑦 ] 𝜓 )
12		vopelopabsb	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 )
13	12	notbii	⊢ ( ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ¬ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 )
14	9 11 13	3bitr4ri	⊢ ( ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ¬ 𝜓 )
15	8 14	anbi12i	⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ¬ 𝜓 ) )
16	5 7 15	3bitr4ri	⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ( 𝜑 ∧ ¬ 𝜓 ) )
17		eldif	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ¬ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
18		vopelopabsb	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ ¬ 𝜓 ) } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ( 𝜑 ∧ ¬ 𝜓 ) )
19	16 17 18	3bitr4i	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ ¬ 𝜓 ) } )
20	3 4 19	eqrelriiv	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ ¬ 𝜓 ) }