Metamath Proof Explorer

Theorem unielid

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

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

Proof

Step Hyp Ref Expression
1 ssid 
 |-  A C_ A
2 unielss 
 |-  ( A C_ A -> ( U. A e. A <-> E. x e. A A. y e. A y C_ x ) )
3 1 2 ax-mp 
 |-  ( U. A e. A <-> E. x e. A A. y e. A y C_ x )