Metamath Proof Explorer


Theorem rexdifpr

Description: Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018) (Proof shortened by Wolf Lammen, 15-May-2025)

Ref Expression
Assertion rexdifpr xABCφxAxBxCφ

Proof

Step Hyp Ref Expression
1 anass xAxBxCφxAxBxCφ
2 eldifpr xABCxAxBxC
3 3anass xAxBxCxAxBxC
4 2 3 bitri xABCxAxBxC
5 4 anbi1i xABCφxAxBxCφ
6 df-3an xBxCφxBxCφ
7 6 anbi2i xAxBxCφxAxBxCφ
8 1 5 7 3bitr4i xABCφxAxBxCφ
9 8 rexbii2 xABCφxAxBxCφ