Metamath Proof Explorer


Theorem ssdifcl

Description: The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020)

Ref Expression
Hypothesis ssficl.a 𝐴 = { 𝑧𝑧𝐵 }
Assertion ssdifcl 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴

Proof

Step Hyp Ref Expression
1 ssficl.a 𝐴 = { 𝑧𝑧𝐵 }
2 vex 𝑥 ∈ V
3 2 difexi ( 𝑥𝑦 ) ∈ V
4 sseq1 ( 𝑧 = ( 𝑥𝑦 ) → ( 𝑧𝐵 ↔ ( 𝑥𝑦 ) ⊆ 𝐵 ) )
5 sseq1 ( 𝑧 = 𝑥 → ( 𝑧𝐵𝑥𝐵 ) )
6 sseq1 ( 𝑧 = 𝑦 → ( 𝑧𝐵𝑦𝐵 ) )
7 ssdifss ( 𝑥𝐵 → ( 𝑥𝑦 ) ⊆ 𝐵 )
8 7 adantr ( ( 𝑥𝐵𝑦𝐵 ) → ( 𝑥𝑦 ) ⊆ 𝐵 )
9 1 3 4 5 6 8 cllem0 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴