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∈ABφ↔ψ∨χ

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 ⊢AB=A∪B
6 5 rexeqi ⊢∃x∈ABφ↔∃x∈A∪Bφ
7 rexun ⊢∃x∈A∪Bφ↔∃x∈Aφ∨∃x∈Bφ
8 6 7 bitri ⊢∃x∈ABφ↔∃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∈ABφ↔ψ∨χ