Metamath Proof Explorer


Theorem elrab2

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006)

Ref Expression
Hypotheses elrab2.1 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
elrab2.2 𝐶 = { 𝑥𝐵𝜑 }
Assertion elrab2 ( 𝐴𝐶 ↔ ( 𝐴𝐵𝜓 ) )

Proof

Step Hyp Ref Expression
1 elrab2.1 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
2 elrab2.2 𝐶 = { 𝑥𝐵𝜑 }
3 2 eleq2i ( 𝐴𝐶𝐴 ∈ { 𝑥𝐵𝜑 } )
4 1 elrab ( 𝐴 ∈ { 𝑥𝐵𝜑 } ↔ ( 𝐴𝐵𝜓 ) )
5 3 4 bitri ( 𝐴𝐶 ↔ ( 𝐴𝐵𝜓 ) )