Metamath Proof Explorer


Theorem predun

Description: Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011)

Ref Expression
Assertion predun Pred R A B X = Pred R A X Pred R B X

Proof

Step Hyp Ref Expression
1 indir A B R -1 X = A R -1 X B R -1 X
2 df-pred Pred R A B X = A B R -1 X
3 df-pred Pred R A X = A R -1 X
4 df-pred Pred R B X = B R -1 X
5 3 4 uneq12i Pred R A X Pred R B X = A R -1 X B R -1 X
6 1 2 5 3eqtr4i Pred R A B X = Pred R A X Pred R B X