Step |
Hyp |
Ref |
Expression |
1 |
|
df-pred |
|- Pred ( _E , A , X ) = ( A i^i ( `' _E " { X } ) ) |
2 |
|
relcnv |
|- Rel `' _E |
3 |
|
relimasn |
|- ( Rel `' _E -> ( `' _E " { X } ) = { y | X `' _E y } ) |
4 |
2 3
|
ax-mp |
|- ( `' _E " { X } ) = { y | X `' _E y } |
5 |
|
brcnvg |
|- ( ( X e. B /\ y e. _V ) -> ( X `' _E y <-> y _E X ) ) |
6 |
5
|
elvd |
|- ( X e. B -> ( X `' _E y <-> y _E X ) ) |
7 |
|
epelg |
|- ( X e. B -> ( y _E X <-> y e. X ) ) |
8 |
6 7
|
bitrd |
|- ( X e. B -> ( X `' _E y <-> y e. X ) ) |
9 |
8
|
abbi1dv |
|- ( X e. B -> { y | X `' _E y } = X ) |
10 |
4 9
|
eqtrid |
|- ( X e. B -> ( `' _E " { X } ) = X ) |
11 |
10
|
ineq2d |
|- ( X e. B -> ( A i^i ( `' _E " { X } ) ) = ( A i^i X ) ) |
12 |
1 11
|
eqtrid |
|- ( X e. B -> Pred ( _E , A , X ) = ( A i^i X ) ) |