Metamath Proof Explorer


Theorem eltrpred

Description: A class is a transitive predecessor iff it is in some value of the underlying function. This theorem is not meant to be used directly; use trpredpred and trpredmintr instead. (Contributed by Scott Fenton, 28-Apr-2012)

Ref Expression
Assertion eltrpred Y TrPred R A X i ω Y rec a V y a Pred R A y Pred R A X ω i

Proof

Step Hyp Ref Expression
1 dftrpred2 TrPred R A X = i ω rec a V y a Pred R A y Pred R A X ω i
2 1 eleq2i Y TrPred R A X Y i ω rec a V y a Pred R A y Pred R A X ω i
3 eliun Y i ω rec a V y a Pred R A y Pred R A X ω i i ω Y rec a V y a Pred R A y Pred R A X ω i
4 2 3 bitri Y TrPred R A X i ω Y rec a V y a Pred R A y Pred R A X ω i