Metamath Proof Explorer


Theorem opelopaba

Description: The law of concretion. Theorem 9.5 of Quine p. 61. (Contributed by Mario Carneiro, 19-Dec-2013)

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

Proof

Step Hyp Ref Expression
1 opelopaba.1 𝐴 ∈ V
2 opelopaba.2 𝐵 ∈ V
3 opelopaba.3 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜓 ) )
4 3 opelopabga ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜓 ) )
5 1 2 4 mp2an ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜓 )