Theorem sn-tz6.12-2

Description: tz6.12-2 without ax-10 , ax-11 , ax-12 . Improves 118 theorems. (Contributed by SN, 27-May-2025)

	Ref	Expression
Assertion	sn-tz6.12-2	$$⊢\neg \exists !xAFx\to F\left(A\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢x=y\to \left(AFx\leftrightarrow AFy\right)$$
2		breq2	$$⊢x=z\to \left(AFx\leftrightarrow AFz\right)$$
3	1 2	euabsn2w	$$⊢\exists !xAFx\leftrightarrow \exists y\left\{x|AFx\right\}=\left\{y\right\}$$
4	3	notbii	$$⊢\neg \exists !xAFx\leftrightarrow \neg \exists y\left\{x|AFx\right\}=\left\{y\right\}$$
5		df-fv	$$⊢F\left(A\right)=\left(\iota x|AFx\right)$$
6		iotanul2	$$⊢\neg \exists y\left\{x|AFx\right\}=\left\{y\right\}\to \left(\iota x|AFx\right)=\varnothing$$
7	5 6	eqtrid	$$⊢\neg \exists y\left\{x|AFx\right\}=\left\{y\right\}\to F\left(A\right)=\varnothing$$
8	4 7	sylbi	$$⊢\neg \exists !xAFx\to F\left(A\right)=\varnothing$$