Metamath Proof Explorer

Theorem rexprgf

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

Ref Expression
Hypotheses ralprgf.1 ⊢ Ⅎ x ψ
ralprgf.2 ⊢ Ⅎ x χ
ralprgf.a ⊢ x = A → φ ↔ ψ
ralprgf.b ⊢ x = B → φ ↔ χ
Assertion rexprgf ⊢ 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 rexeqi ⊢ ∃ x ∈ A B φ ↔ ∃ x ∈ A ∪ B φ
7 rexun ⊢ ∃ x ∈ A ∪ B φ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ B φ
8 6 7 bitri ⊢ ∃ x ∈ A B φ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ B φ
9 1 3 rexsngf ⊢ A ∈ V → ∃ x ∈ A φ ↔ ψ
10 9 orbi1d ⊢ A ∈ V → ∃ x ∈ A φ ∨ ∃ x ∈ B φ ↔ ψ ∨ ∃ x ∈ B φ
11 2 4 rexsngf ⊢ B ∈ W → ∃ x ∈ B φ ↔ χ
12 11 orbi2d ⊢ B ∈ W → ψ ∨ ∃ x ∈ B φ ↔ ψ ∨ χ
13 10 12 sylan9bb ⊢ A ∈ V ∧ B ∈ W → ∃ x ∈ A φ ∨ ∃ x ∈ B φ ↔ ψ ∨ χ
14 8 13 bitrid ⊢ A ∈ V ∧ B ∈ W → ∃ x ∈ A B φ ↔ ψ ∨ χ