Metamath Proof Explorer


Theorem psrbagfOLD

Description: Obsolete version of psrbag as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis psrbag.d D = f 0 I | f -1 Fin
Assertion psrbagfOLD I V F D F : I 0

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 1 psrbag I V F D F : I 0 F -1 Fin
3 2 simprbda I V F D F : I 0