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

Metamath Proof Explorer

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 )