Step |
Hyp |
Ref |
Expression |
1 |
|
dftrpred2 |
|- TrPred ( R , A , X ) = U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) |
2 |
1
|
eleq2i |
|- ( Y e. TrPred ( R , A , X ) <-> Y e. U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) |
3 |
|
eliun |
|- ( Y e. U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) <-> E. i e. _om Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) |
4 |
2 3
|
bitri |
|- ( Y e. TrPred ( R , A , X ) <-> E. i e. _om Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) |