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 GG, 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	⊢ ( 𝑥 𝑅 𝑦 ↔ 𝜑 )