Theorem brabsb2

Description: A closed form of brabsb . (Contributed by Rodolfo Medina, 13-Oct-2010)

	Ref	Expression
Assertion	brabsb2	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( 𝑧 𝑅 𝑤 ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		breq	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( 𝑧 𝑅 𝑤 ↔ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑤 ) )
2		df-br	⊢ ( 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
3	1 2	bitrdi	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( 𝑧 𝑅 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
4		vopelopabsb	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
5	3 4	bitrdi	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( 𝑧 𝑅 𝑤 ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )