Theorem newval

Description: The value of the new options function. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	newval	⊢ ( 𝐴 ∈ On → ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐴 → ( M ‘ 𝑥 ) = ( M ‘ 𝐴 ) )
2		fveq2	⊢ ( 𝑥 = 𝐴 → ( O ‘ 𝑥 ) = ( O ‘ 𝐴 ) )
3	1 2	difeq12d	⊢ ( 𝑥 = 𝐴 → ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )
4		df-new	⊢ N = ( 𝑥 ∈ On ↦ ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) )
5		fvex	⊢ ( M ‘ 𝐴 ) ∈ V
6	5	difexi	⊢ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ∈ V
7	3 4 6	fvmpt	⊢ ( 𝐴 ∈ On → ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )