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 in place of bm1.3ii . Relabel ("sepbi"?).

	Ref	Expression
Assertion	bj-bm1.3ii	|- ( E. x A. z ( ph -> z e. x ) <-> E. y A. z ( z e. y <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		elequ2	|- ( x = t -> ( z e. x <-> z e. t ) )
2	1	imbi2d	|- ( x = t -> ( ( ph -> z e. x ) <-> ( ph -> z e. t ) ) )
3	2	albidv	|- ( x = t -> ( A. z ( ph -> z e. x ) <-> A. z ( ph -> z e. t ) ) )
4	3	cbvexvw	|- ( E. x A. z ( ph -> z e. x ) <-> E. t A. z ( ph -> z e. t ) )
5		ax-sep	|- E. y A. z ( z e. y <-> ( z e. t /\ ph ) )
6		19.42v	|- ( E. y ( A. z ( ph -> z e. t ) /\ A. z ( z e. y <-> ( z e. t /\ ph ) ) ) <-> ( A. z ( ph -> z e. t ) /\ E. y A. z ( z e. y <-> ( z e. t /\ ph ) ) ) )
7		bimsc1	|- ( ( ( ph -> z e. t ) /\ ( z e. y <-> ( z e. t /\ ph ) ) ) -> ( z e. y <-> ph ) )
8	7	alanimi	|- ( ( A. z ( ph -> z e. t ) /\ A. z ( z e. y <-> ( z e. t /\ ph ) ) ) -> A. z ( z e. y <-> ph ) )
9	8	eximi	|- ( E. y ( A. z ( ph -> z e. t ) /\ A. z ( z e. y <-> ( z e. t /\ ph ) ) ) -> E. y A. z ( z e. y <-> ph ) )
10	6 9	sylbir	|- ( ( A. z ( ph -> z e. t ) /\ E. y A. z ( z e. y <-> ( z e. t /\ ph ) ) ) -> E. y A. z ( z e. y <-> ph ) )
11	5 10	mpan2	|- ( A. z ( ph -> z e. t ) -> E. y A. z ( z e. y <-> ph ) )
12	11	exlimiv	|- ( E. t A. z ( ph -> z e. t ) -> E. y A. z ( z e. y <-> ph ) )
13		elequ2	|- ( y = t -> ( z e. y <-> z e. t ) )
14	13	bibi1d	|- ( y = t -> ( ( z e. y <-> ph ) <-> ( z e. t <-> ph ) ) )
15	14	albidv	|- ( y = t -> ( A. z ( z e. y <-> ph ) <-> A. z ( z e. t <-> ph ) ) )
16	15	cbvexvw	|- ( E. y A. z ( z e. y <-> ph ) <-> E. t A. z ( z e. t <-> ph ) )
17		biimpr	|- ( ( z e. t <-> ph ) -> ( ph -> z e. t ) )
18	17	alimi	|- ( A. z ( z e. t <-> ph ) -> A. z ( ph -> z e. t ) )
19	18	eximi	|- ( E. t A. z ( z e. t <-> ph ) -> E. t A. z ( ph -> z e. t ) )
20	16 19	sylbi	|- ( E. y A. z ( z e. y <-> ph ) -> E. t A. z ( ph -> z e. t ) )
21	12 20	impbii	|- ( E. t A. z ( ph -> z e. t ) <-> E. y A. z ( z e. y <-> ph ) )
22	4 21	bitri	|- ( E. x A. z ( ph -> z e. x ) <-> E. y A. z ( z e. y <-> ph ) )