This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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\} \in Fin$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$⊢ \{A, B\} = \{A\} \cup \{B\}$
2		snfi	$⊢ \{A\} \in Fin$
3		snfi	$⊢ \{B\} \in Fin$
4		unfi	$⊢ (\{A\} \in Fin \land \{B\} \in Fin) \to \{A\} \cup \{B\} \in Fin$
5	2 3 4	mp2an	$⊢ \{A\} \cup \{B\} \in Fin$
6	1 5	eqeltri	$⊢ \{A, B\} \in Fin$