Metamath Proof Explorer

Theorem predprc

Description: The predecessor of a proper class is empty. (Contributed by Scott Fenton, 25-Nov-2024)

Ref Expression
Assertion predprc 
|- ( -. X e. _V -> Pred ( R , A , X ) = (/) )

Proof

Step Hyp Ref Expression
1 df-pred 
 |-  Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
2 snprc 
 |-  ( -. X e. _V <-> { X } = (/) )
3 2 biimpi 
 |-  ( -. X e. _V -> { X } = (/) )
4 3 imaeq2d 
 |-  ( -. X e. _V -> ( `' R " { X } ) = ( `' R " (/) ) )
5 ima0 
 |-  ( `' R " (/) ) = (/)
6 4 5 eqtrdi 
 |-  ( -. X e. _V -> ( `' R " { X } ) = (/) )
7 6 ineq2d 
 |-  ( -. X e. _V -> ( A i^i ( `' R " { X } ) ) = ( A i^i (/) ) )
8 in0 
 |-  ( A i^i (/) ) = (/)
9 7 8 eqtrdi 
 |-  ( -. X e. _V -> ( A i^i ( `' R " { X } ) ) = (/) )
10 1 9 eqtrid 
 |-  ( -. X e. _V -> Pred ( R , A , X ) = (/) )