Theorem bj-ru0 32932

Description: The FOL part of Russell's paradox ru 3434 (see also bj-ru1 32933, bj-ru 32934). Use of elequ1 1997, bj-elequ12 32668, bj-spvv 32723 (instead of eleq1 2689, eleq12d 2695, spv 2260 as in ru 3434) permits to remove dependency on ax-10 2019, ax-11 2034, ax-12 2047, ax-13 2246, ax-ext 2602, df-sb 1881, df-clab 2609, df-cleq 2615, df-clel 2618. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-ru0	|- -. A. x ( x e. y <-> -. x e. x )

Distinct variable group:   x, y

Proof of Theorem bj-ru0

Step	Hyp	Ref	Expression
1		pm5.19 375	. 2 |- -. ( y e. y <-> -. y e. y )
2		elequ1 1997	. . . 4 |- ( x = y -> ( x e. y <-> y e. y ) )
3		bj-elequ12 32668	. . . . . 6 |- ( ( x = y /\ x = y ) -> ( x e. x <-> y e. y ) )
4	3	anidms 677	. . . . 5 |- ( x = y -> ( x e. x <-> y e. y ) )
5	4	notbid 308	. . . 4 |- ( x = y -> ( -. x e. x <-> -. y e. y ) )
6	2, 5	bibi12d 335	. . 3 |- ( x = y -> ( ( x e. y <-> -. x e. x ) <-> ( y e. y <-> -. y e. y ) ) )
7	6	bj-spvv 32723	. 2 |- ( A. x ( x e. y <-> -. x e. x ) -> ( y e. y <-> -. y e. y ) )
8	1, 7	mto 188	1 |- -. A. x ( x e. y <-> -. x e. x )

Syntax hints:   -. wn 3   <-> wb 196   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  bj-ru1  32933