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 𝑥 𝜓
opelopabf.y 𝑦 𝜒
opelopabf.1 𝐴 ∈ V
opelopabf.2 𝐵 ∈ V
opelopabf.3 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
opelopabf.4 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) )
Assertion opelopabf ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 )

Proof

Step Hyp Ref Expression
1 opelopabf.x 𝑥 𝜓
2 opelopabf.y 𝑦 𝜒
3 opelopabf.1 𝐴 ∈ V
4 opelopabf.2 𝐵 ∈ V
5 opelopabf.3 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
6 opelopabf.4 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) )
7 opelopabsb ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )
8 nfcv 𝑥 𝐵
9 8 1 nfsbcw 𝑥 [ 𝐵 / 𝑦 ] 𝜓
10 5 sbcbidv ( 𝑥 = 𝐴 → ( [ 𝐵 / 𝑦 ] 𝜑[ 𝐵 / 𝑦 ] 𝜓 ) )
11 9 10 sbciegf ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑[ 𝐵 / 𝑦 ] 𝜓 ) )
12 3 11 ax-mp ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑[ 𝐵 / 𝑦 ] 𝜓 )
13 2 6 sbciegf ( 𝐵 ∈ V → ( [ 𝐵 / 𝑦 ] 𝜓𝜒 ) )
14 4 13 ax-mp ( [ 𝐵 / 𝑦 ] 𝜓𝜒 )
15 7 12 14 3bitri ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 )