Theorem 2ralbida

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 24-Feb-2004)

	Ref	Expression
Hypotheses	2ralbida.1	⊢ Ⅎ 𝑥 𝜑
	2ralbida.2	⊢ Ⅎ 𝑦 𝜑
	2ralbida.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	2ralbida	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		2ralbida.1	⊢ Ⅎ 𝑥 𝜑
2		2ralbida.2	⊢ Ⅎ 𝑦 𝜑
3		2ralbida.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
4		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
5	2 4	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
6	3	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
7	5 6	ralbida	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 𝜓 ↔ ∀ 𝑦 ∈ 𝐵 𝜒 ) )
8	1 7	ralbida	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜒 ) )