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φ→∃zz⊆B∧∀x∈A∃y∈zφ

Proof

Step Hyp Ref Expression
1 bnd2.1 ⊢A∈V
2 df-rex ⊢∃y∈Bφ↔∃yy∈B∧φ
3 2 ralbii ⊢∀x∈A∃y∈Bφ↔∀x∈A∃yy∈B∧φ
4 raleq ⊢v=A→∀x∈v∃yy∈B∧φ↔∀x∈A∃yy∈B∧φ
5 raleq ⊢v=A→∀x∈v∃y∈wy∈B∧φ↔∀x∈A∃y∈wy∈B∧φ
6 5 exbidv ⊢v=A→∃w∀x∈v∃y∈wy∈B∧φ↔∃w∀x∈A∃y∈wy∈B∧φ
7 4 6 imbi12d ⊢v=A→∀x∈v∃yy∈B∧φ→∃w∀x∈v∃y∈wy∈B∧φ↔∀x∈A∃yy∈B∧φ→∃w∀x∈A∃y∈wy∈B∧φ
8 bnd ⊢∀x∈v∃yy∈B∧φ→∃w∀x∈v∃y∈wy∈B∧φ
9 1 7 8 vtocl ⊢∀x∈A∃yy∈B∧φ→∃w∀x∈A∃y∈wy∈B∧φ
10 3 9 sylbi ⊢∀x∈A∃y∈Bφ→∃w∀x∈A∃y∈wy∈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∈wy∈B∧φ
19 17 18 bitrdi ⊢z=w∩B→∃y∈zφ↔∃y∈wy∈B∧φ
20 19 ralbidv ⊢z=w∩B→∀x∈A∃y∈zφ↔∀x∈A∃y∈wy∈B∧φ
21 16 20 bitr3d ⊢z=w∩B→z⊆B∧∀x∈A∃y∈zφ↔∀x∈A∃y∈wy∈B∧φ
22 12 21 spcev ⊢∀x∈A∃y∈wy∈B∧φ→∃zz⊆B∧∀x∈A∃y∈zφ
23 22 exlimiv ⊢∃w∀x∈A∃y∈wy∈B∧φ→∃zz⊆B∧∀x∈A∃y∈zφ
24 10 23 syl ⊢∀x∈A∃y∈Bφ→∃zz⊆B∧∀x∈A∃y∈zφ