Metamath Proof Explorer


Theorem sspred

Description: Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011)

Ref Expression
Assertion sspred BAPredRAXBPredRAX=PredRBX

Proof

Step Hyp Ref Expression
1 sseqin2 BAAB=B
2 df-pred PredRAX=AR-1X
3 2 sseq1i PredRAXBAR-1XB
4 df-ss AR-1XBAR-1XB=AR-1X
5 in32 AR-1XB=ABR-1X
6 5 eqeq1i AR-1XB=AR-1XABR-1X=AR-1X
7 3 4 6 3bitri PredRAXBABR-1X=AR-1X
8 ineq1 AB=BABR-1X=BR-1X
9 8 eqeq1d AB=BABR-1X=AR-1XBR-1X=AR-1X
10 9 biimpa AB=BABR-1X=AR-1XBR-1X=AR-1X
11 df-pred PredRBX=BR-1X
12 10 11 2 3eqtr4g AB=BABR-1X=AR-1XPredRBX=PredRAX
13 12 eqcomd AB=BABR-1X=AR-1XPredRAX=PredRBX
14 1 7 13 syl2anb BAPredRAXBPredRAX=PredRBX