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 𝐴 ∈ V
Assertion bnd2 ( ∀ 𝑥𝐴𝑦𝐵 𝜑 → ∃ 𝑧 ( 𝑧𝐵 ∧ ∀ 𝑥𝐴𝑦𝑧 𝜑 ) )

Proof

Step Hyp Ref Expression
1 bnd2.1 𝐴 ∈ V
2 df-rex ( ∃ 𝑦𝐵 𝜑 ↔ ∃ 𝑦 ( 𝑦𝐵𝜑 ) )
3 2 ralbii ( ∀ 𝑥𝐴𝑦𝐵 𝜑 ↔ ∀ 𝑥𝐴𝑦 ( 𝑦𝐵𝜑 ) )
4 raleq ( 𝑣 = 𝐴 → ( ∀ 𝑥𝑣𝑦 ( 𝑦𝐵𝜑 ) ↔ ∀ 𝑥𝐴𝑦 ( 𝑦𝐵𝜑 ) ) )
5 raleq ( 𝑣 = 𝐴 → ( ∀ 𝑥𝑣𝑦𝑤 ( 𝑦𝐵𝜑 ) ↔ ∀ 𝑥𝐴𝑦𝑤 ( 𝑦𝐵𝜑 ) ) )
6 5 exbidv ( 𝑣 = 𝐴 → ( ∃ 𝑤𝑥𝑣𝑦𝑤 ( 𝑦𝐵𝜑 ) ↔ ∃ 𝑤𝑥𝐴𝑦𝑤 ( 𝑦𝐵𝜑 ) ) )
7 4 6 imbi12d ( 𝑣 = 𝐴 → ( ( ∀ 𝑥𝑣𝑦 ( 𝑦𝐵𝜑 ) → ∃ 𝑤𝑥𝑣𝑦𝑤 ( 𝑦𝐵𝜑 ) ) ↔ ( ∀ 𝑥𝐴𝑦 ( 𝑦𝐵𝜑 ) → ∃ 𝑤𝑥𝐴𝑦𝑤 ( 𝑦𝐵𝜑 ) ) ) )
8 bnd ( ∀ 𝑥𝑣𝑦 ( 𝑦𝐵𝜑 ) → ∃ 𝑤𝑥𝑣𝑦𝑤 ( 𝑦𝐵𝜑 ) )
9 1 7 8 vtocl ( ∀ 𝑥𝐴𝑦 ( 𝑦𝐵𝜑 ) → ∃ 𝑤𝑥𝐴𝑦𝑤 ( 𝑦𝐵𝜑 ) )
10 3 9 sylbi ( ∀ 𝑥𝐴𝑦𝐵 𝜑 → ∃ 𝑤𝑥𝐴𝑦𝑤 ( 𝑦𝐵𝜑 ) )
11 vex 𝑤 ∈ V
12 11 inex1 ( 𝑤𝐵 ) ∈ V
13 inss2 ( 𝑤𝐵 ) ⊆ 𝐵
14 sseq1 ( 𝑧 = ( 𝑤𝐵 ) → ( 𝑧𝐵 ↔ ( 𝑤𝐵 ) ⊆ 𝐵 ) )
15 13 14 mpbiri ( 𝑧 = ( 𝑤𝐵 ) → 𝑧𝐵 )
16 15 biantrurd ( 𝑧 = ( 𝑤𝐵 ) → ( ∀ 𝑥𝐴𝑦𝑧 𝜑 ↔ ( 𝑧𝐵 ∧ ∀ 𝑥𝐴𝑦𝑧 𝜑 ) ) )
17 rexeq ( 𝑧 = ( 𝑤𝐵 ) → ( ∃ 𝑦𝑧 𝜑 ↔ ∃ 𝑦 ∈ ( 𝑤𝐵 ) 𝜑 ) )
18 rexin ( ∃ 𝑦 ∈ ( 𝑤𝐵 ) 𝜑 ↔ ∃ 𝑦𝑤 ( 𝑦𝐵𝜑 ) )
19 17 18 bitrdi ( 𝑧 = ( 𝑤𝐵 ) → ( ∃ 𝑦𝑧 𝜑 ↔ ∃ 𝑦𝑤 ( 𝑦𝐵𝜑 ) ) )
20 19 ralbidv ( 𝑧 = ( 𝑤𝐵 ) → ( ∀ 𝑥𝐴𝑦𝑧 𝜑 ↔ ∀ 𝑥𝐴𝑦𝑤 ( 𝑦𝐵𝜑 ) ) )
21 16 20 bitr3d ( 𝑧 = ( 𝑤𝐵 ) → ( ( 𝑧𝐵 ∧ ∀ 𝑥𝐴𝑦𝑧 𝜑 ) ↔ ∀ 𝑥𝐴𝑦𝑤 ( 𝑦𝐵𝜑 ) ) )
22 12 21 spcev ( ∀ 𝑥𝐴𝑦𝑤 ( 𝑦𝐵𝜑 ) → ∃ 𝑧 ( 𝑧𝐵 ∧ ∀ 𝑥𝐴𝑦𝑧 𝜑 ) )
23 22 exlimiv ( ∃ 𝑤𝑥𝐴𝑦𝑤 ( 𝑦𝐵𝜑 ) → ∃ 𝑧 ( 𝑧𝐵 ∧ ∀ 𝑥𝐴𝑦𝑧 𝜑 ) )
24 10 23 syl ( ∀ 𝑥𝐴𝑦𝐵 𝜑 → ∃ 𝑧 ( 𝑧𝐵 ∧ ∀ 𝑥𝐴𝑦𝑧 𝜑 ) )