Theorem r19.26m

Description: Version of 19.26 and r19.26 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004)

	Ref	Expression
Assertion	r19.26m	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 → 𝜓 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		19.26	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 → 𝜓 ) ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜓 ) ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
3		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜓 ) )
4	2 3	anbi12i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 𝜓 ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜓 ) ) )
5	1 4	bitr4i	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 → 𝜓 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 𝜓 ) )