Theorem bj-bm1.3ii

Description: The extension of a predicate ( ph ( z ) ) is included in a set ( x ) if and only if it is a set ( y ). Sufficiency is obvious, and necessity is the content of the axiom of separation ax-sep . Similar to Theorem 1.3(ii) of BellMachover p. 463. (Contributed by NM, 21-Jun-1993) Generalized to a closed form biconditional with existential quantifications using two different setvars x , y (which need not be disjoint). (Revised by BJ, 8-Aug-2022)

TODO: move after sepexi . Relabel ("sepbi"?).

	Ref	Expression
Assertion	bj-bm1.3ii	$$⊢\exists x\forall z\left(\phi \to z\in x\right)\leftrightarrow \exists y\forall z\left(z\in y\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elequ2	$$⊢x=t\to \left(z\in x\leftrightarrow z\in t\right)$$
2	1	imbi2d	$$⊢x=t\to \left(\left(\phi \to z\in x\right)\leftrightarrow \left(\phi \to z\in t\right)\right)$$
3	2	albidv	$$⊢x=t\to \left(\forall z\left(\phi \to z\in x\right)\leftrightarrow \forall z\left(\phi \to z\in t\right)\right)$$
4	3	cbvexvw	$$⊢\exists x\forall z\left(\phi \to z\in x\right)\leftrightarrow \exists t\forall z\left(\phi \to z\in t\right)$$
5		ax-sep	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \left(z\in t\wedge \phi \right)\right)$$
6		19.42v	$$⊢\exists y\left(\forall z\left(\phi \to z\in t\right)\wedge \forall z\left(z\in y\leftrightarrow \left(z\in t\wedge \phi \right)\right)\right)\leftrightarrow \left(\forall z\left(\phi \to z\in t\right)\wedge \exists y\forall z\left(z\in y\leftrightarrow \left(z\in t\wedge \phi \right)\right)\right)$$
7		bimsc1	$$⊢\left(\left(\phi \to z\in t\right)\wedge \left(z\in y\leftrightarrow \left(z\in t\wedge \phi \right)\right)\right)\to \left(z\in y\leftrightarrow \phi \right)$$
8	7	alanimi	$$⊢\left(\forall z\left(\phi \to z\in t\right)\wedge \forall z\left(z\in y\leftrightarrow \left(z\in t\wedge \phi \right)\right)\right)\to \forall z\left(z\in y\leftrightarrow \phi \right)$$
9	8	eximi	$$⊢\exists y\left(\forall z\left(\phi \to z\in t\right)\wedge \forall z\left(z\in y\leftrightarrow \left(z\in t\wedge \phi \right)\right)\right)\to \exists y\forall z\left(z\in y\leftrightarrow \phi \right)$$
10	6 9	sylbir	$$⊢\left(\forall z\left(\phi \to z\in t\right)\wedge \exists y\forall z\left(z\in y\leftrightarrow \left(z\in t\wedge \phi \right)\right)\right)\to \exists y\forall z\left(z\in y\leftrightarrow \phi \right)$$
11	5 10	mpan2	$$⊢\forall z\left(\phi \to z\in t\right)\to \exists y\forall z\left(z\in y\leftrightarrow \phi \right)$$
12	11	exlimiv	$$⊢\exists t\forall z\left(\phi \to z\in t\right)\to \exists y\forall z\left(z\in y\leftrightarrow \phi \right)$$
13		elequ2	$$⊢y=t\to \left(z\in y\leftrightarrow z\in t\right)$$
14	13	bibi1d	$$⊢y=t\to \left(\left(z\in y\leftrightarrow \phi \right)\leftrightarrow \left(z\in t\leftrightarrow \phi \right)\right)$$
15	14	albidv	$$⊢y=t\to \left(\forall z\left(z\in y\leftrightarrow \phi \right)\leftrightarrow \forall z\left(z\in t\leftrightarrow \phi \right)\right)$$
16	15	cbvexvw	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \phi \right)\leftrightarrow \exists t\forall z\left(z\in t\leftrightarrow \phi \right)$$
17		biimpr	$$⊢\left(z\in t\leftrightarrow \phi \right)\to \left(\phi \to z\in t\right)$$
18	17	alimi	$$⊢\forall z\left(z\in t\leftrightarrow \phi \right)\to \forall z\left(\phi \to z\in t\right)$$
19	18	eximi	$$⊢\exists t\forall z\left(z\in t\leftrightarrow \phi \right)\to \exists t\forall z\left(\phi \to z\in t\right)$$
20	16 19	sylbi	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \phi \right)\to \exists t\forall z\left(\phi \to z\in t\right)$$
21	12 20	impbii	$$⊢\exists t\forall z\left(\phi \to z\in t\right)\leftrightarrow \exists y\forall z\left(z\in y\leftrightarrow \phi \right)$$
22	4 21	bitri	$$⊢\exists x\forall z\left(\phi \to z\in x\right)\leftrightarrow \exists y\forall z\left(z\in y\leftrightarrow \phi \right)$$