Theorem bnd2d

Description: Deduction form of bnd2 . (Contributed by Emmett Weisz, 19-Jan-2021)

	Ref	Expression
Hypotheses	bnd2d.1	|- ( ph -> A e. _V )
	bnd2d.2	|- ( ph -> A. x e. A E. y e. B ps )
Assertion	bnd2d	|- ( ph -> E. z ( z C_ B /\ A. x e. A E. y e. z ps ) )

Proof

Step	Hyp	Ref	Expression
1		bnd2d.1	|- ( ph -> A e. _V )
2		bnd2d.2	|- ( ph -> A. x e. A E. y e. B ps )
3		raleq	|- ( A = if ( A e. _V , A , (/) ) -> ( A. x e. A E. y e. B ps <-> A. x e. if ( A e. _V , A , (/) ) E. y e. B ps ) )
4		raleq	|- ( A = if ( A e. _V , A , (/) ) -> ( A. x e. A E. y e. z ps <-> A. x e. if ( A e. _V , A , (/) ) E. y e. z ps ) )
5	4	anbi2d	|- ( A = if ( A e. _V , A , (/) ) -> ( ( z C_ B /\ A. x e. A E. y e. z ps ) <-> ( z C_ B /\ A. x e. if ( A e. _V , A , (/) ) E. y e. z ps ) ) )
6	5	exbidv	|- ( A = if ( A e. _V , A , (/) ) -> ( E. z ( z C_ B /\ A. x e. A E. y e. z ps ) <-> E. z ( z C_ B /\ A. x e. if ( A e. _V , A , (/) ) E. y e. z ps ) ) )
7	3 6	imbi12d	|- ( A = if ( A e. _V , A , (/) ) -> ( ( A. x e. A E. y e. B ps -> E. z ( z C_ B /\ A. x e. A E. y e. z ps ) ) <-> ( A. x e. if ( A e. _V , A , (/) ) E. y e. B ps -> E. z ( z C_ B /\ A. x e. if ( A e. _V , A , (/) ) E. y e. z ps ) ) ) )
8		0ex	|- (/) e. _V
9	8	elimel	|- if ( A e. _V , A , (/) ) e. _V
10	9	bnd2	|- ( A. x e. if ( A e. _V , A , (/) ) E. y e. B ps -> E. z ( z C_ B /\ A. x e. if ( A e. _V , A , (/) ) E. y e. z ps ) )
11	7 10	dedth	|- ( A e. _V -> ( A. x e. A E. y e. B ps -> E. z ( z C_ B /\ A. x e. A E. y e. z ps ) ) )
12	1 2 11	sylc	|- ( ph -> E. z ( z C_ B /\ A. x e. A E. y e. z ps ) )