Metamath Proof Explorer


Theorem abeqinbi

Description: Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 abeqinbi.1 𝐴 = ( 𝐵𝐶 )
2 abeqinbi.2 𝐵 = { 𝑥𝜑 }
3 abeqinbi.3 ( 𝑥𝐶 → ( 𝜑𝜓 ) )
4 1 2 abeqin 𝐴 = { 𝑥𝐶𝜑 }
5 4 3 rabimbieq 𝐴 = { 𝑥𝐶𝜓 }