Metamath Proof Explorer

Theorem opelopabt

Description: Closed theorem form of opelopab . (Contributed by NM, 19-Feb-2013)

Ref Expression
Assertion opelopabt ⊢∀x∀yx=A→φ↔ψ∧∀x∀yy=B→ψ↔χ∧A∈V∧B∈W→AB∈xy|φ↔χ

Proof

Step Hyp Ref Expression
1 elopab ⊢AB∈xy|φ↔∃x∃yAB=xy∧φ
2 19.26-2 ⊢∀x∀yx=A→φ↔ψ∧y=B→ψ↔χ↔∀x∀yx=A→φ↔ψ∧∀x∀yy=B→ψ↔χ
3 anim12 ⊢x=A→φ↔ψ∧y=B→ψ↔χ→x=A∧y=B→φ↔ψ∧ψ↔χ
4 bitr ⊢φ↔ψ∧ψ↔χ→φ↔χ
5 3 4 syl6 ⊢x=A→φ↔ψ∧y=B→ψ↔χ→x=A∧y=B→φ↔χ
6 5 2alimi ⊢∀x∀yx=A→φ↔ψ∧y=B→ψ↔χ→∀x∀yx=A∧y=B→φ↔χ
7 2 6 sylbir ⊢∀x∀yx=A→φ↔ψ∧∀x∀yy=B→ψ↔χ→∀x∀yx=A∧y=B→φ↔χ
8 copsex2t ⊢∀x∀yx=A∧y=B→φ↔χ∧A∈V∧B∈W→∃x∃yAB=xy∧φ↔χ
9 7 8 stoic3 ⊢∀x∀yx=A→φ↔ψ∧∀x∀yy=B→ψ↔χ∧A∈V∧B∈W→∃x∃yAB=xy∧φ↔χ
10 1 9 bitrid ⊢∀x∀yx=A→φ↔ψ∧∀x∀yy=B→ψ↔χ∧A∈V∧B∈W→AB∈xy|φ↔χ