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 V
Assertion bnd2 x A y B φ z z B x A y z φ

Proof

Step Hyp Ref Expression
1 bnd2.1 A V
2 df-rex y B φ y y B φ
3 2 ralbii x A y B φ x A y y B φ
4 raleq v = A x v y y B φ x A y y B φ
5 raleq v = A x v y w y B φ x A y w y B φ
6 5 exbidv v = A w x v y w y B φ w x A y w y B φ
7 4 6 imbi12d v = A x v y y B φ w x v y w y B φ x A y y B φ w x A y w y B φ
8 bnd x v y y B φ w x v y w y B φ
9 1 7 8 vtocl x A y y B φ w x A y w y B φ
10 3 9 sylbi x A y B φ w x A y w y B φ
11 vex w V
12 11 inex1 w B V
13 inss2 w B B
14 sseq1 z = w B z B w B B
15 13 14 mpbiri z = w B z B
16 15 biantrurd z = w B x A y z φ z B x A y z φ
17 rexeq z = w B y z φ y w B φ
18 rexin y w B φ y w y B φ
19 17 18 bitrdi z = w B y z φ y w y B φ
20 19 ralbidv z = w B x A y z φ x A y w y B φ
21 16 20 bitr3d z = w B z B x A y z φ x A y w y B φ
22 12 21 spcev x A y w y B φ z z B x A y z φ
23 22 exlimiv w x A y w y B φ z z B x A y z φ
24 10 23 syl x A y B φ z z B x A y z φ