Theorem r19.42v

Description: Restricted quantifier version of 19.42v (see also 19.42 ). (Contributed by NM, 27-May-1998)

	Ref	Expression
Assertion	r19.42v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.41v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ 𝜑 ) )
2		ancom	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝜑 ) )
3	2	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ 𝜑 ) )
4		ancom	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ 𝜑 ) )
5	1 3 4	3bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ) )