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	⊢ { 𝐴 , 𝐵 } ∈ Fin

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2		snfi	⊢ { 𝐴 } ∈ Fin
3		snfi	⊢ { 𝐵 } ∈ Fin
4		unfi	⊢ ( ( { 𝐴 } ∈ Fin ∧ { 𝐵 } ∈ Fin ) → ( { 𝐴 } ∪ { 𝐵 } ) ∈ Fin )
5	2 3 4	mp2an	⊢ ( { 𝐴 } ∪ { 𝐵 } ) ∈ Fin
6	1 5	eqeltri	⊢ { 𝐴 , 𝐵 } ∈ Fin