Theorem bnd2

Description: A variant of the Boundedness Axiom bnd that picks a subset z out of a possibly proper class B in which a property is true. (Contributed by NM, 4-Feb-2004)

	Ref	Expression
Hypothesis	bnd2.1	|- A e. _V
Assertion	bnd2	|- ( A. x e. A E. y e. B ph -> E. z ( z C_ B /\ A. x e. A E. y e. z ph ) )

Proof

Step	Hyp	Ref	Expression
1		bnd2.1	|- A e. _V
2		df-rex	|- ( E. y e. B ph <-> E. y ( y e. B /\ ph ) )
3	2	ralbii	|- ( A. x e. A E. y e. B ph <-> A. x e. A E. y ( y e. B /\ ph ) )
4		raleq	|- ( v = A -> ( A. x e. v E. y ( y e. B /\ ph ) <-> A. x e. A E. y ( y e. B /\ ph ) ) )
5		raleq	|- ( v = A -> ( A. x e. v E. y e. w ( y e. B /\ ph ) <-> A. x e. A E. y e. w ( y e. B /\ ph ) ) )
6	5	exbidv	|- ( v = A -> ( E. w A. x e. v E. y e. w ( y e. B /\ ph ) <-> E. w A. x e. A E. y e. w ( y e. B /\ ph ) ) )
7	4 6	imbi12d	|- ( v = A -> ( ( A. x e. v E. y ( y e. B /\ ph ) -> E. w A. x e. v E. y e. w ( y e. B /\ ph ) ) <-> ( A. x e. A E. y ( y e. B /\ ph ) -> E. w A. x e. A E. y e. w ( y e. B /\ ph ) ) ) )
8		bnd	|- ( A. x e. v E. y ( y e. B /\ ph ) -> E. w A. x e. v E. y e. w ( y e. B /\ ph ) )
9	1 7 8	vtocl	|- ( A. x e. A E. y ( y e. B /\ ph ) -> E. w A. x e. A E. y e. w ( y e. B /\ ph ) )
10	3 9	sylbi	|- ( A. x e. A E. y e. B ph -> E. w A. x e. A E. y e. w ( y e. B /\ ph ) )
11		vex	|- w e. _V
12	11	inex1	|- ( w i^i B ) e. _V
13		inss2	|- ( w i^i B ) C_ B
14		sseq1	|- ( z = ( w i^i B ) -> ( z C_ B <-> ( w i^i B ) C_ B ) )
15	13 14	mpbiri	|- ( z = ( w i^i B ) -> z C_ B )
16	15	biantrurd	|- ( z = ( w i^i B ) -> ( A. x e. A E. y e. z ph <-> ( z C_ B /\ A. x e. A E. y e. z ph ) ) )
17		rexeq	|- ( z = ( w i^i B ) -> ( E. y e. z ph <-> E. y e. ( w i^i B ) ph ) )
18		rexin	|- ( E. y e. ( w i^i B ) ph <-> E. y e. w ( y e. B /\ ph ) )
19	17 18	bitrdi	|- ( z = ( w i^i B ) -> ( E. y e. z ph <-> E. y e. w ( y e. B /\ ph ) ) )
20	19	ralbidv	|- ( z = ( w i^i B ) -> ( A. x e. A E. y e. z ph <-> A. x e. A E. y e. w ( y e. B /\ ph ) ) )
21	16 20	bitr3d	|- ( z = ( w i^i B ) -> ( ( z C_ B /\ A. x e. A E. y e. z ph ) <-> A. x e. A E. y e. w ( y e. B /\ ph ) ) )
22	12 21	spcev	|- ( A. x e. A E. y e. w ( y e. B /\ ph ) -> E. z ( z C_ B /\ A. x e. A E. y e. z ph ) )
23	22	exlimiv	|- ( E. w A. x e. A E. y e. w ( y e. B /\ ph ) -> E. z ( z C_ B /\ A. x e. A E. y e. z ph ) )
24	10 23	syl	|- ( A. x e. A E. y e. B ph -> E. z ( z C_ B /\ A. x e. A E. y e. z ph ) )