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 } e. Fin

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { A , B } = ( { A } u. { B } )
2		snfi	|- { A } e. Fin
3		snfi	|- { B } e. Fin
4		unfi	|- ( ( { A } e. Fin /\ { B } e. Fin ) -> ( { A } u. { B } ) e. Fin )
5	2 3 4	mp2an	|- ( { A } u. { B } ) e. Fin
6	1 5	eqeltri	|- { A , B } e. Fin