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 ⊢φ→∃zz⊆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=ifA∈VA∅→∀x∈A∃y∈Bψ↔∀x∈ifA∈VA∅∃y∈Bψ
4 raleq ⊢A=ifA∈VA∅→∀x∈A∃y∈zψ↔∀x∈ifA∈VA∅∃y∈zψ
5 4 anbi2d ⊢A=ifA∈VA∅→z⊆B∧∀x∈A∃y∈zψ↔z⊆B∧∀x∈ifA∈VA∅∃y∈zψ
6 5 exbidv ⊢A=ifA∈VA∅→∃zz⊆B∧∀x∈A∃y∈zψ↔∃zz⊆B∧∀x∈ifA∈VA∅∃y∈zψ
7 3 6 imbi12d ⊢A=ifA∈VA∅→∀x∈A∃y∈Bψ→∃zz⊆B∧∀x∈A∃y∈zψ↔∀x∈ifA∈VA∅∃y∈Bψ→∃zz⊆B∧∀x∈ifA∈VA∅∃y∈zψ
8 0ex ⊢∅∈V
9 8 elimel ⊢ifA∈VA∅∈V
10 9 bnd2 ⊢∀x∈ifA∈VA∅∃y∈Bψ→∃zz⊆B∧∀x∈ifA∈VA∅∃y∈zψ
11 7 10 dedth ⊢A∈V→∀x∈A∃y∈Bψ→∃zz⊆B∧∀x∈A∃y∈zψ
12 1 2 11 sylc ⊢φ→∃zz⊆B∧∀x∈A∃y∈zψ