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

Metamath Proof Explorer

Theorem r19.28v

Description: Restricted quantifier version of one direction of 19.28 . (Assuming F/_ x A , the other direction holds when A is nonempty, see r19.28zv .) (Contributed by NM, 2-Apr-2004) (Proof shortened by Wolf Lammen, 17-Jun-2023)

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

Proof

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