Theorem bnj89

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj89.1	$$⊢Z\in \mathrm{V}$$
Assertion	bnj89	$$⊢\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\exists !x\phi \leftrightarrow \exists !x\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		bnj89.1	$$⊢Z\in \mathrm{V}$$
2		sbcex2	$$⊢\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\exists w\forall x\left(\phi \leftrightarrow x=w\right)\leftrightarrow \exists w\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\forall x\left(\phi \leftrightarrow x=w\right)$$
3		sbcal	$$⊢\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\forall x\left(\phi \leftrightarrow x=w\right)\leftrightarrow \forall x\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\left(\phi \leftrightarrow x=w\right)$$
4	3	exbii	$$⊢\exists w\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\forall x\left(\phi \leftrightarrow x=w\right)\leftrightarrow \exists w\forall x\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\left(\phi \leftrightarrow x=w\right)$$
5		sbcbig	$$⊢Z\in \mathrm{V}\to \left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\left(\phi \leftrightarrow x=w\right)\leftrightarrow \left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}Z/y\underset{\dot{}}{]}x=w\right)\right)$$
6	1 5	ax-mp	$$⊢\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\left(\phi \leftrightarrow x=w\right)\leftrightarrow \left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}Z/y\underset{\dot{}}{]}x=w\right)$$
7		sbcg	$$⊢Z\in \mathrm{V}\to \left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}x=w\leftrightarrow x=w\right)$$
8	1 7	ax-mp	$$⊢\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}x=w\leftrightarrow x=w$$
9	8	bibi2i	$$⊢\left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}Z/y\underset{\dot{}}{]}x=w\right)\leftrightarrow \left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow x=w\right)$$
10	6 9	bitri	$$⊢\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\left(\phi \leftrightarrow x=w\right)\leftrightarrow \left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow x=w\right)$$
11	10	albii	$$⊢\forall x\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\left(\phi \leftrightarrow x=w\right)\leftrightarrow \forall x\left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow x=w\right)$$
12	11	exbii	$$⊢\exists w\forall x\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\left(\phi \leftrightarrow x=w\right)\leftrightarrow \exists w\forall x\left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow x=w\right)$$
13	2 4 12	3bitri	$$⊢\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\exists w\forall x\left(\phi \leftrightarrow x=w\right)\leftrightarrow \exists w\forall x\left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow x=w\right)$$
14		eu6	$$⊢\exists !x\phi \leftrightarrow \exists w\forall x\left(\phi \leftrightarrow x=w\right)$$
15	14	sbcbii	$$⊢\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\exists !x\phi \leftrightarrow \underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\exists w\forall x\left(\phi \leftrightarrow x=w\right)$$
16		eu6	$$⊢\exists !x\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow \exists w\forall x\left(\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi \leftrightarrow x=w\right)$$
17	13 15 16	3bitr4i	$$⊢\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\exists !x\phi \leftrightarrow \exists !x\underset{\dot{}}{[}Z/y\underset{\dot{}}{]}\phi$$