Metamath Proof Explorer


Theorem opelopabga

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

Ref Expression
Hypothesis opelopabga.1 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜓 ) )
Assertion opelopabga ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 opelopabga.1 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜓 ) )
2 elopab ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
3 1 copsex2g ( ( 𝐴𝑉𝐵𝑊 ) → ( ∃ 𝑥𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ 𝜓 ) )
4 2 3 bitrid ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜓 ) )