Theorem bnd2d

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

	Ref	Expression
Hypotheses	bnd2d.1	⊢ ( 𝜑 → 𝐴 ∈ V )
	bnd2d.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
Assertion	bnd2d	⊢ ( 𝜑 → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		bnd2d.1	⊢ ( 𝜑 → 𝐴 ∈ V )
2		bnd2d.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
3		raleq	⊢ ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ↔ ∀ 𝑥 ∈ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∃ 𝑦 ∈ 𝐵 𝜓 ) )
4		raleq	⊢ ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜓 ↔ ∀ 𝑥 ∈ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∃ 𝑦 ∈ 𝑧 𝜓 ) )
5	4	anbi2d	⊢ ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → ( ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜓 ) ↔ ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∃ 𝑦 ∈ 𝑧 𝜓 ) ) )
6	5	exbidv	⊢ ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → ( ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜓 ) ↔ ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∃ 𝑦 ∈ 𝑧 𝜓 ) ) )
7	3 6	imbi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ V , 𝐴 , ∅ ) → ( ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜓 ) ) ↔ ( ∀ 𝑥 ∈ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∃ 𝑦 ∈ 𝑧 𝜓 ) ) ) )
8		0ex	⊢ ∅ ∈ V
9	8	elimel	⊢ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∈ V
10	9	bnd2	⊢ ( ∀ 𝑥 ∈ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∃ 𝑦 ∈ 𝑧 𝜓 ) )
11	7 10	dedth	⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜓 ) ) )
12	1 2 11	sylc	⊢ ( 𝜑 → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜓 ) )