Theorem newbdayim

Description: One direction of the biconditional in newbday . (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Assertion	newbdayim	⊢ ( 𝑋 ∈ ( N ‘ 𝐴 ) → ( bday ‘ 𝑋 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝑋 ∈ ( N ‘ 𝐴 ) → 𝐴 ∈ dom N )
2		newf	⊢ N : On ⟶ 𝒫 No
3		fdm	⊢ ( N : On ⟶ 𝒫 No → dom N = On )
4	2 3	ax-mp	⊢ dom N = On
5	1 4	eleqtrdi	⊢ ( 𝑋 ∈ ( N ‘ 𝐴 ) → 𝐴 ∈ On )
6		newssno	⊢ ( N ‘ 𝐴 ) ⊆ No
7	6	sseli	⊢ ( 𝑋 ∈ ( N ‘ 𝐴 ) → 𝑋 ∈ No )
8		newbday	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) = 𝐴 ) )
9	5 7 8	syl2anc	⊢ ( 𝑋 ∈ ( N ‘ 𝐴 ) → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) = 𝐴 ) )
10	9	ibi	⊢ ( 𝑋 ∈ ( N ‘ 𝐴 ) → ( bday ‘ 𝑋 ) = 𝐴 )