Theorem brab1

Description: Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011)

	Ref	Expression
Assertion	brab1	⊢ ( 𝑥 𝑅 𝐴 ↔ 𝑥 ∈ { 𝑧 ∣ 𝑧 𝑅 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 𝑅 𝐴 ↔ 𝑦 𝑅 𝐴 ) )
2		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝐴 ↔ 𝑥 𝑅 𝐴 ) )
3	1 2	sbcie2g	⊢ ( 𝑥 ∈ V → ( [ 𝑥 / 𝑧 ] 𝑧 𝑅 𝐴 ↔ 𝑥 𝑅 𝐴 ) )
4	3	elv	⊢ ( [ 𝑥 / 𝑧 ] 𝑧 𝑅 𝐴 ↔ 𝑥 𝑅 𝐴 )
5		df-sbc	⊢ ( [ 𝑥 / 𝑧 ] 𝑧 𝑅 𝐴 ↔ 𝑥 ∈ { 𝑧 ∣ 𝑧 𝑅 𝐴 } )
6	4 5	bitr3i	⊢ ( 𝑥 𝑅 𝐴 ↔ 𝑥 ∈ { 𝑧 ∣ 𝑧 𝑅 𝐴 } )