Metamath Proof Explorer


Theorem prfiALT

Description: Shorter proof of prfi using ax-un . (Contributed by NM, 22-Aug-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion prfiALT A B Fin

Proof

Step Hyp Ref Expression
1 df-pr A B = A B
2 snfi A Fin
3 snfi B Fin
4 unfi A Fin B Fin A B Fin
5 2 3 4 mp2an A B Fin
6 1 5 eqeltri A B Fin