Theorem brabidga

Description: The law of concretion for a binary relation. Special case of brabga . Usage of this theorem is discouraged because it depends on ax-13 , see brabidgaw for a weaker version that does not require it. (Contributed by Peter Mazsa, 24-Nov-2018) (New usage is discouraged.)

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

Proof

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