Metamath Proof Explorer

Theorem ralpr

Description: Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ralpr.1 ⊢ A ∈ V
ralpr.2 ⊢ B ∈ V
ralpr.3 ⊢ x = A → φ ↔ ψ
ralpr.4 ⊢ x = B → φ ↔ χ
Assertion ralpr ⊢ ∀ x ∈ A B φ ↔ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 ralpr.1 ⊢ A ∈ V
2 ralpr.2 ⊢ B ∈ V
3 ralpr.3 ⊢ x = A → φ ↔ ψ
4 ralpr.4 ⊢ x = B → φ ↔ χ
5 3 4 ralprg ⊢ A ∈ V ∧ B ∈ V → ∀ x ∈ A B φ ↔ ψ ∧ χ
6 1 2 5 mp2an ⊢ ∀ x ∈ A B φ ↔ ψ ∧ χ