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)

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 eldifpr 
 |-  ( x e. ( A \ { B , C } ) <-> ( x e. A /\ x =/= B /\ x =/= C ) )
2 3anass 
 |-  ( ( x e. A /\ x =/= B /\ x =/= C ) <-> ( x e. A /\ ( x =/= B /\ x =/= C ) ) )
3 1 2 bitri 
 |-  ( x e. ( A \ { B , C } ) <-> ( x e. A /\ ( x =/= B /\ x =/= C ) ) )
4 3 anbi1i 
 |-  ( ( x e. ( A \ { B , C } ) /\ ph ) <-> ( ( x e. A /\ ( x =/= B /\ x =/= C ) ) /\ ph ) )
5 anass 
 |-  ( ( ( x e. A /\ ( x =/= B /\ x =/= 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 bicomi 
 |-  ( ( ( x =/= B /\ x =/= C ) /\ ph ) <-> ( x =/= B /\ x =/= C /\ ph ) )
8 7 anbi2i 
 |-  ( ( x e. A /\ ( ( x =/= B /\ x =/= C ) /\ ph ) ) <-> ( x e. A /\ ( x =/= B /\ x =/= C /\ ph ) ) )
9 5 8 bitri 
 |-  ( ( ( x e. A /\ ( x =/= B /\ x =/= C ) ) /\ ph ) <-> ( x e. A /\ ( x =/= B /\ x =/= C /\ ph ) ) )
10 4 9 bitri 
 |-  ( ( x e. ( A \ { B , C } ) /\ ph ) <-> ( x e. A /\ ( x =/= B /\ x =/= C /\ ph ) ) )
11 10 rexbii2 
 |-  ( E. x e. ( A \ { B , C } ) ph <-> E. x e. A ( x =/= B /\ x =/= C /\ ph ) )