Metamath Proof Explorer

Theorem elunsn

Description: Elementhood in a union with a singleton. (Contributed by Thierry Arnoux, 14-Dec-2023)

Ref Expression
Assertion elunsn 
|- ( A e. V -> ( A e. ( B u. { C } ) <-> ( A e. B \/ A = C ) ) )

Proof

Step Hyp Ref Expression
1 elun 
 |-  ( A e. ( B u. { C } ) <-> ( A e. B \/ A e. { C } ) )
2 elsng 
 |-  ( A e. V -> ( A e. { C } <-> A = C ) )
3 2 orbi2d 
 |-  ( A e. V -> ( ( A e. B \/ A e. { C } ) <-> ( A e. B \/ A = C ) ) )
4 1 3 bitrid 
 |-  ( A e. V -> ( A e. ( B u. { C } ) <-> ( A e. B \/ A = C ) ) )