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

Metamath Proof Explorer

Theorem r2alf

Description: Double restricted universal quantification. For a version based on fewer axioms see r2al . (Contributed by Mario Carneiro, 14-Oct-2016) Use r2allem . (Revised by Wolf Lammen, 9-Jan-2020)

		Ref	Expression
	Hypothesis	r2alf.1	⊢ Ⅎ 𝑦 𝐴
	Assertion	r2alf	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		r2alf.1	⊢ Ⅎ 𝑦 𝐴
2	1	nfcri	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
3	2	19.21	⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜑 ) ) )
4	3	r2allem	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) )