This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nelrdva

Description: Deduce negative membership from an implication. (Contributed by Thierry Arnoux, 27-Nov-2017)

Ref Expression
Hypothesis nelrdva.1 
|- ( ( ph /\ x e. A ) -> x =/= B )
Assertion nelrdva 
|- ( ph -> -. B e. A )

Proof

Step Hyp Ref Expression
1 nelrdva.1 
 |-  ( ( ph /\ x e. A ) -> x =/= B )
2 eqidd 
 |-  ( ( ph /\ B e. A ) -> B = B )
3 eleq1 
 |-  ( x = B -> ( x e. A <-> B e. A ) )
4 3 anbi2d 
 |-  ( x = B -> ( ( ph /\ x e. A ) <-> ( ph /\ B e. A ) ) )
5 neeq1 
 |-  ( x = B -> ( x =/= B <-> B =/= B ) )
6 4 5 imbi12d 
 |-  ( x = B -> ( ( ( ph /\ x e. A ) -> x =/= B ) <-> ( ( ph /\ B e. A ) -> B =/= B ) ) )
7 6 1 vtoclg 
 |-  ( B e. A -> ( ( ph /\ B e. A ) -> B =/= B ) )
8 7 anabsi7 
 |-  ( ( ph /\ B e. A ) -> B =/= B )
9 8 neneqd 
 |-  ( ( ph /\ B e. A ) -> -. B = B )
10 2 9 pm2.65da 
 |-  ( ph -> -. B e. A )