Metamath Proof Explorer

Theorem ssunib

Description: Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025)

Ref Expression
Assertion ssunib 
|- ( A C_ U. B <-> A. x e. A E. y e. B x e. y )

Proof

Step Hyp Ref Expression
1 dfss3 
 |-  ( A C_ U. B <-> A. x e. A x e. U. B )
2 eluni2 
 |-  ( x e. U. B <-> E. y e. B x e. y )
3 2 ralbii 
 |-  ( A. x e. A x e. U. B <-> A. x e. A E. y e. B x e. y )
4 1 3 bitri 
 |-  ( A C_ U. B <-> A. x e. A E. y e. B x e. y )