Step |
Hyp |
Ref |
Expression |
1 |
|
df-pred |
|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) ) |
2 |
1
|
elin2 |
|- ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y e. ( `' R " { X } ) ) ) |
3 |
2
|
baib |
|- ( Y e. A -> ( Y e. Pred ( R , A , X ) <-> Y e. ( `' R " { X } ) ) ) |
4 |
3
|
adantl |
|- ( ( X e. B /\ Y e. A ) -> ( Y e. Pred ( R , A , X ) <-> Y e. ( `' R " { X } ) ) ) |
5 |
|
elimasng |
|- ( ( X e. B /\ Y e. A ) -> ( Y e. ( `' R " { X } ) <-> <. X , Y >. e. `' R ) ) |
6 |
|
df-br |
|- ( X `' R Y <-> <. X , Y >. e. `' R ) |
7 |
5 6
|
bitr4di |
|- ( ( X e. B /\ Y e. A ) -> ( Y e. ( `' R " { X } ) <-> X `' R Y ) ) |
8 |
|
brcnvg |
|- ( ( X e. B /\ Y e. A ) -> ( X `' R Y <-> Y R X ) ) |
9 |
4 7 8
|
3bitrd |
|- ( ( X e. B /\ Y e. A ) -> ( Y e. Pred ( R , A , X ) <-> Y R X ) ) |