Metamath Proof Explorer


Theorem rexab

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014) (Revised by Mario Carneiro, 3-Sep-2015) Reduce axiom usage. (Revised by Gino Giotto, 2-Nov-2024)

Ref Expression
Hypothesis ralab.1 y=xφψ
Assertion rexab xy|φχxψχ

Proof

Step Hyp Ref Expression
1 ralab.1 y=xφψ
2 dfrex2 xy|φχ¬xy|φ¬χ
3 1 ralab xy|φ¬χxψ¬χ
4 2 3 xchbinx xy|φχ¬xψ¬χ
5 imnang xψ¬χx¬ψχ
6 4 5 xchbinx xy|φχ¬x¬ψχ
7 df-ex xψχ¬x¬ψχ
8 6 7 bitr4i xy|φχxψχ