This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opelopabt

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

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

Proof

Step Hyp Ref Expression
1 elopab ⊢ A B ∈ x y | φ ↔ ∃ x ∃ y A B = x y ∧ φ
2 19.26-2 ⊢ ∀ x ∀ y x = A → φ ↔ ψ ∧ y = B → ψ ↔ χ ↔ ∀ x ∀ y x = A → φ ↔ ψ ∧ ∀ x ∀ y y = 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 ∀ y x = A → φ ↔ ψ ∧ y = B → ψ ↔ χ → ∀ x ∀ y x = A ∧ y = B → φ ↔ χ
7 2 6 sylbir ⊢ ∀ x ∀ y x = A → φ ↔ ψ ∧ ∀ x ∀ y y = B → ψ ↔ χ → ∀ x ∀ y x = A ∧ y = B → φ ↔ χ
8 copsex2t ⊢ ∀ x ∀ y x = A ∧ y = B → φ ↔ χ ∧ A ∈ V ∧ B ∈ W → ∃ x ∃ y A B = x y ∧ φ ↔ χ
9 7 8 stoic3 ⊢ ∀ x ∀ y x = A → φ ↔ ψ ∧ ∀ x ∀ y y = B → ψ ↔ χ ∧ A ∈ V ∧ B ∈ W → ∃ x ∃ y A B = x y ∧ φ ↔ χ
10 1 9 bitrid ⊢ ∀ x ∀ y x = A → φ ↔ ψ ∧ ∀ x ∀ y y = B → ψ ↔ χ ∧ A ∈ V ∧ B ∈ W → A B ∈ x y | φ ↔ χ