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

Metamath Proof Explorer

Theorem ra4v

Description: Version of ra4 with a disjoint variable condition, requiring fewer axioms. This is stdpc5v for a restricted domain. (Contributed by BJ, 27-Mar-2020)

		Ref	Expression
	Assertion	ra4v	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.21v	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 ) )
2	1	biimpi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 ) )