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

Metamath Proof Explorer

Theorem opelopabga

Description: The law of concretion. Theorem 9.5 of Quine p. 61. (Contributed by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypothesis opelopabga.1 ⊢ x = A ∧ y = B → φ ↔ ψ
Assertion opelopabga ⊢ A ∈ V ∧ B ∈ W → A B ∈ x y | φ ↔ ψ

Proof

Step Hyp Ref Expression
1 opelopabga.1 ⊢ x = A ∧ y = B → φ ↔ ψ
2 elopab ⊢ A B ∈ x y | φ ↔ ∃ x ∃ y A B = x y ∧ φ
3 1 copsex2g ⊢ A ∈ V ∧ B ∈ W → ∃ x ∃ y A B = x y ∧ φ ↔ ψ
4 2 3 bitrid ⊢ A ∈ V ∧ B ∈ W → A B ∈ x y | φ ↔ ψ