Theorem nelrdva

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

	Ref	Expression
Hypothesis	nelrdva.1	$$⊢\left(\phi \wedge x\in A\right)\to x\ne B$$
Assertion	nelrdva	$$⊢\phi \to \neg B\in A$$

Proof

Step	Hyp	Ref	Expression
1		nelrdva.1	$$⊢\left(\phi \wedge x\in A\right)\to x\ne B$$
2		eqidd	$$⊢\left(\phi \wedge B\in A\right)\to B=B$$
3		eleq1	$$⊢x=B\to \left(x\in A\leftrightarrow B\in A\right)$$
4	3	anbi2d	$$⊢x=B\to \left(\left(\phi \wedge x\in A\right)\leftrightarrow \left(\phi \wedge B\in A\right)\right)$$
5		neeq1	$$⊢x=B\to \left(x\ne B\leftrightarrow B\ne B\right)$$
6	4 5	imbi12d	$$⊢x=B\to \left(\left(\left(\phi \wedge x\in A\right)\to x\ne B\right)\leftrightarrow \left(\left(\phi \wedge B\in A\right)\to B\ne B\right)\right)$$
7	6 1	vtoclg	$$⊢B\in A\to \left(\left(\phi \wedge B\in A\right)\to B\ne B\right)$$
8	7	anabsi7	$$⊢\left(\phi \wedge B\in A\right)\to B\ne B$$
9	8	neneqd	$$⊢\left(\phi \wedge B\in A\right)\to \neg B=B$$
10	2 9	pm2.65da	$$⊢\phi \to \neg B\in A$$