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=f0I|f-1Fin
Assertion psrbagfOLD IVFDF:I0

Proof

Step Hyp Ref Expression
1 psrbag.d D=f0I|f-1Fin
2 1 psrbag IVFDF:I0F-1Fin
3 2 simprbda IVFDF:I0