Theorem rabeq0 3397

Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.)

Assertion

Ref	Expression
rabeq0	|- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )

Proof of Theorem rabeq0

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		imnan 680	. . 3 |- ( ( x e. A -> -. ph ) <-> -. ( x e. A /\ ph ) )
2	1	albii 1447	. 2 |- ( A. x ( x e. A -> -. ph ) <-> A. x -. ( x e. A /\ ph ) )
3		df-ral 2422	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
4		sbn 1926	. . . 4 |- ( [ y / x ] -. ( x e. A /\ ph ) <-> -. [ y / x ] ( x e. A /\ ph ) )
5	4	albii 1447	. . 3 |- ( A. y [ y / x ] -. ( x e. A /\ ph ) <-> A. y -. [ y / x ] ( x e. A /\ ph ) )
6		nfv 1509	. . . 4 |- F/ y -. ( x e. A /\ ph )
7	6	sb8 1829	. . 3 |- ( A. x -. ( x e. A /\ ph ) <-> A. y [ y / x ] -. ( x e. A /\ ph ) )
8		eq0 3386	. . . 4 |- ( { x e. A | ph } = (/) <-> A. y -. y e. { x e. A | ph } )
9		df-rab 2426	. . . . . . . 8 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
10	9	eleq2i 2207	. . . . . . 7 |- ( y e. { x e. A | ph } <-> y e. { x | ( x e. A /\ ph ) } )
11		df-clab 2127	. . . . . . 7 |- ( y e. { x | ( x e. A /\ ph ) } <-> [ y / x ] ( x e. A /\ ph ) )
12	10, 11	bitri 183	. . . . . 6 |- ( y e. { x e. A | ph } <-> [ y / x ] ( x e. A /\ ph ) )
13	12	notbii 658	. . . . 5 |- ( -. y e. { x e. A | ph } <-> -. [ y / x ] ( x e. A /\ ph ) )
14	13	albii 1447	. . . 4 |- ( A. y -. y e. { x e. A | ph } <-> A. y -. [ y / x ] ( x e. A /\ ph ) )
15	8, 14	bitri 183	. . 3 |- ( { x e. A | ph } = (/) <-> A. y -. [ y / x ] ( x e. A /\ ph ) )
16	5, 7, 15	3bitr4ri 212	. 2 |- ( { x e. A | ph } = (/) <-> A. x -. ( x e. A /\ ph ) )
17	2, 3, 16	3bitr4ri 212	1 |- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1330   = wceq 1332   e. wcel 1481   [wsb 1736   {cab 2126   A.wral 2417   {crab 2421   (/)c0 3368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rab 2426  df-v 2691  df-dif 3078  df-nul 3369

This theorem is referenced by:  rabnc  3400  rabrsndc  3599  exmidsssnc  4134  ssfilem  6777  diffitest  6789  ssfirab  6830  ctssexmid  7032  exmidonfinlem  7066  iooidg  9722  icc0r  9739  fznlem  9852  ioo0  10068  ico0  10070  ioc0  10071  phiprmpw  11934  hashgcdeq  11940  unennn  11946  znnen  11947