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	|- ( E. x e. ( A \ { B , C } ) ph <-> E. x e. A ( x =/= B /\ x =/= C /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		anass	|- ( ( ( x e. A /\ ( x =/= B /\ x =/= C ) ) /\ ph ) <-> ( x e. A /\ ( ( x =/= B /\ x =/= C ) /\ ph ) ) )
2		eldifpr	|- ( x e. ( A \ { B , C } ) <-> ( x e. A /\ x =/= B /\ x =/= C ) )
3		3anass	|- ( ( x e. A /\ x =/= B /\ x =/= C ) <-> ( x e. A /\ ( x =/= B /\ x =/= C ) ) )
4	2 3	bitri	|- ( x e. ( A \ { B , C } ) <-> ( x e. A /\ ( x =/= B /\ x =/= C ) ) )
5	4	anbi1i	|- ( ( x e. ( A \ { B , C } ) /\ ph ) <-> ( ( x e. A /\ ( x =/= B /\ x =/= C ) ) /\ ph ) )
6		df-3an	|- ( ( x =/= B /\ x =/= C /\ ph ) <-> ( ( x =/= B /\ x =/= C ) /\ ph ) )
7	6	anbi2i	|- ( ( x e. A /\ ( x =/= B /\ x =/= C /\ ph ) ) <-> ( x e. A /\ ( ( x =/= B /\ x =/= C ) /\ ph ) ) )
8	1 5 7	3bitr4i	|- ( ( x e. ( A \ { B , C } ) /\ ph ) <-> ( x e. A /\ ( x =/= B /\ x =/= C /\ ph ) ) )
9	8	rexbii2	|- ( E. x e. ( A \ { B , C } ) ph <-> E. x e. A ( x =/= B /\ x =/= C /\ ph ) )