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

Metamath Proof Explorer

Theorem opelopabf

Description: The law of concretion. Theorem 9.5 of Quine p. 61. This version of opelopab uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 19-Dec-2008)

Ref Expression
Hypotheses opelopabf.x ⊢ Ⅎ x ψ
opelopabf.y ⊢ Ⅎ y χ
opelopabf.1 ⊢ A ∈ V
opelopabf.2 ⊢ B ∈ V
opelopabf.3 ⊢ x = A → φ ↔ ψ
opelopabf.4 ⊢ y = B → ψ ↔ χ
Assertion opelopabf ⊢ A B ∈ x y | φ ↔ χ

Proof

Step Hyp Ref Expression
1 opelopabf.x ⊢ Ⅎ x ψ
2 opelopabf.y ⊢ Ⅎ y χ
3 opelopabf.1 ⊢ A ∈ V
4 opelopabf.2 ⊢ B ∈ V
5 opelopabf.3 ⊢ x = A → φ ↔ ψ
6 opelopabf.4 ⊢ y = B → ψ ↔ χ
7 opelopabsb ⊢ A B ∈ x y | φ ↔ [˙A / x]˙ [˙B / y]˙ φ
8 nfcv ⊢ Ⅎ _ x B
9 8 1 nfsbcw ⊢ Ⅎ x [˙B / y]˙ ψ
10 5 sbcbidv ⊢ x = A → [˙B / y]˙ φ ↔ [˙B / y]˙ ψ
11 9 10 sbciegf ⊢ A ∈ V → [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ ψ
12 3 11 ax-mp ⊢ [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ ψ
13 2 6 sbciegf ⊢ B ∈ V → [˙B / y]˙ ψ ↔ χ
14 4 13 ax-mp ⊢ [˙B / y]˙ ψ ↔ χ
15 7 12 14 3bitri ⊢ A B ∈ x y | φ ↔ χ