Metamath Proof Explorer

Theorem bnd2d

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

Ref Expression
Hypotheses bnd2d.1 ⊢ φ → A ∈ V
bnd2d.2 ⊢ φ → ∀ x ∈ A ∃ y ∈ B ψ
Assertion bnd2d ⊢ φ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z ψ

Proof

Step Hyp Ref Expression
1 bnd2d.1 ⊢ φ → A ∈ V
2 bnd2d.2 ⊢ φ → ∀ x ∈ A ∃ y ∈ B ψ
3 raleq ⊢ A = if A ∈ V A ∅ → ∀ x ∈ A ∃ y ∈ B ψ ↔ ∀ x ∈ if A ∈ V A ∅ ∃ y ∈ B ψ
4 raleq ⊢ A = if A ∈ V A ∅ → ∀ x ∈ A ∃ y ∈ z ψ ↔ ∀ x ∈ if A ∈ V A ∅ ∃ y ∈ z ψ
5 4 anbi2d ⊢ A = if A ∈ V A ∅ → z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z ψ ↔ z ⊆ B ∧ ∀ x ∈ if A ∈ V A ∅ ∃ y ∈ z ψ
6 5 exbidv ⊢ A = if A ∈ V A ∅ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z ψ ↔ ∃ z z ⊆ B ∧ ∀ x ∈ if A ∈ V A ∅ ∃ y ∈ z ψ
7 3 6 imbi12d ⊢ A = if A ∈ V A ∅ → ∀ x ∈ A ∃ y ∈ B ψ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z ψ ↔ ∀ x ∈ if A ∈ V A ∅ ∃ y ∈ B ψ → ∃ z z ⊆ B ∧ ∀ x ∈ if A ∈ V A ∅ ∃ y ∈ z ψ
8 0ex ⊢ ∅ ∈ V
9 8 elimel ⊢ if A ∈ V A ∅ ∈ V
10 9 bnd2 ⊢ ∀ x ∈ if A ∈ V A ∅ ∃ y ∈ B ψ → ∃ z z ⊆ B ∧ ∀ x ∈ if A ∈ V A ∅ ∃ y ∈ z ψ
11 7 10 dedth ⊢ A ∈ V → ∀ x ∈ A ∃ y ∈ B ψ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z ψ
12 1 2 11 sylc ⊢ φ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z ψ