Metamath Proof Explorer

Theorem tpid3g

Description: Closed theorem form of tpid3 . (Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by JJ, 30-Apr-2021)

Ref Expression
Assertion tpid3g 
|- ( A e. B -> A e. { C , D , A } )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 1 3mix3i 
 |-  ( A = C \/ A = D \/ A = A )
3 eltpg 
 |-  ( A e. B -> ( A e. { C , D , A } <-> ( A = C \/ A = D \/ A = A ) ) )
4 2 3 mpbiri 
 |-  ( A e. B -> A e. { C , D , A } )