Metamath Proof Explorer

Theorem elpredg

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011)

Ref Expression
Assertion elpredg 
|- ( ( X e. B /\ Y e. A ) -> ( Y e. Pred ( R , A , X ) <-> Y R X ) )

Proof

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 ) )