Metamath Proof Explorer

Theorem ralprgf

Description: Convert a restricted universal quantification over a pair to a conjunction, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 17-Sep-2011) (Revised by AV, 8-Apr-2023)

Ref Expression
Hypotheses ralprgf.1 ⊢ Ⅎ x ψ
ralprgf.2 ⊢ Ⅎ x χ
ralprgf.a ⊢ x = A → φ ↔ ψ
ralprgf.b ⊢ x = B → φ ↔ χ
Assertion ralprgf ⊢ A ∈ V ∧ B ∈ W → ∀ x ∈ A B φ ↔ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 ralprgf.1 ⊢ Ⅎ x ψ
2 ralprgf.2 ⊢ Ⅎ x χ
3 ralprgf.a ⊢ x = A → φ ↔ ψ
4 ralprgf.b ⊢ x = B → φ ↔ χ
5 df-pr ⊢ A B = A ∪ B
6 5 raleqi ⊢ ∀ x ∈ A B φ ↔ ∀ x ∈ A ∪ B φ
7 ralunb ⊢ ∀ x ∈ A ∪ B φ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ B φ
8 6 7 bitri ⊢ ∀ x ∈ A B φ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ B φ
9 1 3 ralsngf ⊢ A ∈ V → ∀ x ∈ A φ ↔ ψ
10 2 4 ralsngf ⊢ B ∈ W → ∀ x ∈ B φ ↔ χ
11 9 10 bi2anan9 ⊢ A ∈ V ∧ B ∈ W → ∀ x ∈ A φ ∧ ∀ x ∈ B φ ↔ ψ ∧ χ
12 8 11 bitrid ⊢ A ∈ V ∧ B ∈ W → ∀ x ∈ A B φ ↔ ψ ∧ χ