Metamath Proof Explorer


Theorem brabidgaw

Description: The law of concretion for a binary relation. Special case of brabga . Version of brabidga with a disjoint variable condition, which does not require ax-13 . (Contributed by Peter Mazsa, 24-Nov-2018) (Revised by Gino Giotto, 2-Apr-2024)

Ref Expression
Hypothesis brabidgaw.1 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
Assertion brabidgaw ( 𝑥 𝑅 𝑦𝜑 )

Proof

Step Hyp Ref Expression
1 brabidgaw.1 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2 1 breqi ( 𝑥 𝑅 𝑦𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 )
3 df-br ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
4 opabidw ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
5 2 3 4 3bitri ( 𝑥 𝑅 𝑦𝜑 )