Theorem sn-subf

Description: subf without ax-mulcom . (Contributed by SN, 5-May-2024)

	Ref	Expression
Assertion	sn-subf	$$⊢-:ℂ\times ℂ⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		subval	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x-y=\left(\iota z\in ℂ|y+z=x\right)$$
2		sn-subcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x-y\in ℂ$$
3	1 2	eqeltrrd	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \left(\iota z\in ℂ|y+z=x\right)\in ℂ$$
4	3	rgen2	$$⊢\forall x\in ℂ\forall y\in ℂ\left(\iota z\in ℂ|y+z=x\right)\in ℂ$$
5		df-sub	$$⊢-=\left(x\in ℂ,y\in ℂ⟼\left(\iota z\in ℂ|y+z=x\right)\right)$$
6	5	fmpo	$$⊢\forall x\in ℂ\forall y\in ℂ\left(\iota z\in ℂ|y+z=x\right)\in ℂ\leftrightarrow -:ℂ\times ℂ⟶ℂ$$
7	4 6	mpbi	$$⊢-:ℂ\times ℂ⟶ℂ$$