Theorem eliincex

Description: Counterexample to show that the additional conditions in eliin and eliin2 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	eliinct.1	|- A = _V
	eliinct.2	|- B = (/)
Assertion	eliincex	|- -. ( A e. |^|_ x e. B C <-> A. x e. B A e. C )

Proof

Step	Hyp	Ref	Expression
1		eliinct.1	|- A = _V
2		eliinct.2	|- B = (/)
3		nvel	|- -. _V e. |^|_ x e. B C
4	1 3	eqneltri	|- -. A e. |^|_ x e. B C
5		ral0	|- A. x e. (/) A e. C
6	2	raleqi	|- ( A. x e. B A e. C <-> A. x e. (/) A e. C )
7	5 6	mpbir	|- A. x e. B A e. C
8		pm3.22	|- ( ( -. A e. |^|_ x e. B C /\ A. x e. B A e. C ) -> ( A. x e. B A e. C /\ -. A e. |^|_ x e. B C ) )
9	8	olcd	|- ( ( -. A e. |^|_ x e. B C /\ A. x e. B A e. C ) -> ( ( A e. |^|_ x e. B C /\ -. A. x e. B A e. C ) \/ ( A. x e. B A e. C /\ -. A e. |^|_ x e. B C ) ) )
10		xor	|- ( -. ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) <-> ( ( A e. |^|_ x e. B C /\ -. A. x e. B A e. C ) \/ ( A. x e. B A e. C /\ -. A e. |^|_ x e. B C ) ) )
11	9 10	sylibr	|- ( ( -. A e. |^|_ x e. B C /\ A. x e. B A e. C ) -> -. ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
12	4 7 11	mp2an	|- -. ( A e. |^|_ x e. B C <-> A. x e. B A e. C )