Metamath Proof Explorer


Theorem rabeq2i

Description: Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004)

Ref Expression
Hypothesis rabeq2i.1 𝐴 = { 𝑥𝐵𝜑 }
Assertion rabeq2i ( 𝑥𝐴 ↔ ( 𝑥𝐵𝜑 ) )

Proof

Step Hyp Ref Expression
1 rabeq2i.1 𝐴 = { 𝑥𝐵𝜑 }
2 1 eleq2i ( 𝑥𝐴𝑥 ∈ { 𝑥𝐵𝜑 } )
3 rabid ( 𝑥 ∈ { 𝑥𝐵𝜑 } ↔ ( 𝑥𝐵𝜑 ) )
4 2 3 bitri ( 𝑥𝐴 ↔ ( 𝑥𝐵𝜑 ) )