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 ⊢ Ⅎ 𝑥 𝜓
opelopabgf.y ⊢ Ⅎ 𝑦 𝜒
opelopabgf.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
opelopabgf.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
Assertion opelopabgf ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 opelopabgf.x ⊢ Ⅎ 𝑥 𝜓
2 opelopabgf.y ⊢ Ⅎ 𝑦 𝜒
3 opelopabgf.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4 opelopabgf.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
5 opelopabsb ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )
6 nfcv ⊢ Ⅎ 𝑥 𝐵
7 6 1 nfsbcw ⊢ Ⅎ 𝑥 [ 𝐵 / 𝑦 ] 𝜓
8 3 sbcbidv ⊢ ( 𝑥 = 𝐴 → ( [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] 𝜓 ) )
9 7 8 sbciegf ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] 𝜓 ) )
10 2 4 sbciegf ⊢ ( 𝐵 ∈ 𝑊 → ( [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )
11 9 10 sylan9bb ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ 𝜒 ) )
12 5 11 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )