Metamath Proof Explorer

Theorem tpid1g

Description: Closed theorem form of tpid1 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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