This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )