Theorem exintrbi

Description: Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006)

	Ref	Expression
Assertion	exintrbi	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		abai	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( 𝜑 → 𝜓 ) ) )
2	1	rbaibr	⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 ↔ ( 𝜑 ∧ 𝜓 ) ) )
3	2	alexbii	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )