Metamath Proof Explorer

Theorem ralprg

Description: Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011) (Revised by Mario Carneiro, 23-Apr-2015) Avoid ax-10 , ax-12 . (Revised by GG, 30-Sep-2024)

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

Proof

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