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

Metamath Proof Explorer

Theorem opelopabgf

Description: The law of concretion. Theorem 9.5 of Quine p. 61. This version of opelopabg uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Alexander van der Vekens, 8-Jul-2018)

Ref Expression
Hypotheses opelopabgf.x ⊢ Ⅎ x ψ
opelopabgf.y ⊢ Ⅎ y χ
opelopabgf.1 ⊢ x = A → φ ↔ ψ
opelopabgf.2 ⊢ y = B → ψ ↔ χ
Assertion opelopabgf ⊢ A ∈ V ∧ B ∈ W → A B ∈ x y | φ ↔ χ

Proof

Step Hyp Ref Expression
1 opelopabgf.x ⊢ Ⅎ x ψ
2 opelopabgf.y ⊢ Ⅎ y χ
3 opelopabgf.1 ⊢ x = A → φ ↔ ψ
4 opelopabgf.2 ⊢ y = B → ψ ↔ χ
5 opelopabsb ⊢ A B ∈ x y | φ ↔ [˙A / x]˙ [˙B / y]˙ φ
6 nfcv ⊢ Ⅎ _ x B
7 6 1 nfsbcw ⊢ Ⅎ x [˙B / y]˙ ψ
8 3 sbcbidv ⊢ x = A → [˙B / y]˙ φ ↔ [˙B / y]˙ ψ
9 7 8 sbciegf ⊢ A ∈ V → [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ ψ
10 2 4 sbciegf ⊢ B ∈ W → [˙B / y]˙ ψ ↔ χ
11 9 10 sylan9bb ⊢ A ∈ V ∧ B ∈ W → [˙A / x]˙ [˙B / y]˙ φ ↔ χ
12 5 11 bitrid ⊢ A ∈ V ∧ B ∈ W → A B ∈ x y | φ ↔ χ