Metamath Proof Explorer


Theorem opelopabaf

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 Mario Carneiro, 19-Dec-2013) (Proof shortened by Mario Carneiro, 18-Nov-2016)

Ref Expression
Hypotheses opelopabaf.x 𝑥 𝜓
opelopabaf.y 𝑦 𝜓
opelopabaf.1 𝐴 ∈ V
opelopabaf.2 𝐵 ∈ V
opelopabaf.3 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜓 ) )
Assertion opelopabaf ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜓 )

Proof

Step Hyp Ref Expression
1 opelopabaf.x 𝑥 𝜓
2 opelopabaf.y 𝑦 𝜓
3 opelopabaf.1 𝐴 ∈ V
4 opelopabaf.2 𝐵 ∈ V
5 opelopabaf.3 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜓 ) )
6 opelopabsb ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )
7 nfv 𝑥 𝐵 ∈ V
8 1 2 7 5 sbc2iegf ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑𝜓 ) )
9 3 4 8 mp2an ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑𝜓 )
10 6 9 bitri ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜓 )