Metamath Proof Explorer


Theorem inelros

Description: A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020)

Ref Expression
Hypothesis isros.1 Q=s𝒫𝒫O|sxsysxysxys
Assertion inelros SQASBSABS

Proof

Step Hyp Ref Expression
1 isros.1 Q=s𝒫𝒫O|sxsysxysxys
2 dfin4 AB=AAB
3 1 difelros SQASBSABS
4 1 difelros SQASABSAABS
5 3 4 syld3an3 SQASBSAABS
6 2 5 eqeltrid SQASBSABS