Theorem nnexALT

Description: Alternate proof of nnex , more direct, that makes use of ax-rep . (Contributed by Mario Carneiro, 3-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nnexALT	⊢ ℕ ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-nn	⊢ ℕ = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω )
2		rdgfun	⊢ Fun rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 )
3		omex	⊢ ω ∈ V
4		funimaexg	⊢ ( ( Fun rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ∧ ω ∈ V ) → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) ∈ V )
5	2 3 4	mp2an	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) ∈ V
6	1 5	eqeltri	⊢ ℕ ∈ V