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

Metamath Proof Explorer

Theorem r19.27v

Description: Restricted quantitifer version of one direction of 19.27 . (Assuming F/_ x A , the other direction holds when A is nonempty, see r19.27zv .) (Contributed by NM, 3-Jun-2004) (Proof shortened by Andrew Salmon, 30-May-2011) (Proof shortened by Wolf Lammen, 17-Jun-2023)

		Ref	Expression
	Assertion	r19.27v	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝜓 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝜓 → 𝜓 )
2	1	ralrimivw	⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 𝜓 )
3	2	anim2i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝜓 ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
4		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
5	3 4	sylibr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝜓 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) )