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 A=BC
abeqinbi.2 B=x|φ
abeqinbi.3 xCφψ
Assertion abeqinbi A=xC|ψ

Proof

Step Hyp Ref Expression
1 abeqinbi.1 A=BC
2 abeqinbi.2 B=x|φ
3 abeqinbi.3 xCφψ
4 1 2 abeqin A=xC|φ
5 4 3 rabimbieq A=xC|ψ