This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r19.41

Description: Restricted quantifier version of 19.41 . See r19.41v for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010)

		Ref	Expression
	Hypothesis	r19.41.1	⊢ Ⅎ 𝑥 𝜓
	Assertion	r19.41	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.41.1	⊢ Ⅎ 𝑥 𝜓
2		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) )
3		anass	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) )
4	3	exbii	⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜓 ) ) )
5	1	19.41	⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝜓 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝜓 ) )
6		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
7	6	bicomi	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
8	5 7	bianbi	⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ 𝜓 ) )
9	2 4 8	3bitr2i	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ 𝜓 ) )