Metamath Proof Explorer

Theorem brab1

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

Ref Expression
Assertion brab1 ⊢ x R A ↔ x ∈ z | z R A

Proof

Step Hyp Ref Expression
1 breq1 ⊢ z = y → z R A ↔ y R A
2 breq1 ⊢ y = x → y R A ↔ x R A
3 1 2 sbcie2g ⊢ x ∈ V → [˙x / z]˙ z R A ↔ x R A
4 3 elv ⊢ [˙x / z]˙ z R A ↔ x R A
5 df-sbc ⊢ [˙x / z]˙ z R A ↔ x ∈ z | z R A
6 4 5 bitr3i ⊢ x R A ↔ x ∈ z | z R A