Theorem rabeq0 3476

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 691	. . 3 |- ( ( x e. A -> -. ph ) <-> -. ( x e. A /\ ph ) )
2	1	albii 1481	. 2 |- ( A. x ( x e. A -> -. ph ) <-> A. x -. ( x e. A /\ ph ) )
3		df-ral 2477	. 2 |- ( A. x e. A -. ph <-> A. x ( x e. A -> -. ph ) )
4		sbn 1968	. . . 4 |- ( [ y / x ] -. ( x e. A /\ ph ) <-> -. [ y / x ] ( x e. A /\ ph ) )
5	4	albii 1481	. . 3 |- ( A. y [ y / x ] -. ( x e. A /\ ph ) <-> A. y -. [ y / x ] ( x e. A /\ ph ) )
6		nfv 1539	. . . 4 |- F/ y -. ( x e. A /\ ph )
7	6	sb8 1867	. . 3 |- ( A. x -. ( x e. A /\ ph ) <-> A. y [ y / x ] -. ( x e. A /\ ph ) )
8		eq0 3465	. . . 4 |- ( { x e. A | ph } = (/) <-> A. y -. y e. { x e. A | ph } )
9		df-rab 2481	. . . . . . . 8 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
10	9	eleq2i 2260	. . . . . . 7 |- ( y e. { x e. A | ph } <-> y e. { x | ( x e. A /\ ph ) } )
11		df-clab 2180	. . . . . . 7 |- ( y e. { x | ( x e. A /\ ph ) } <-> [ y / x ] ( x e. A /\ ph ) )
12	10, 11	bitri 184	. . . . . 6 |- ( y e. { x e. A | ph } <-> [ y / x ] ( x e. A /\ ph ) )
13	12	notbii 669	. . . . 5 |- ( -. y e. { x e. A | ph } <-> -. [ y / x ] ( x e. A /\ ph ) )
14	13	albii 1481	. . . 4 |- ( A. y -. y e. { x e. A | ph } <-> A. y -. [ y / x ] ( x e. A /\ ph ) )
15	8, 14	bitri 184	. . 3 |- ( { x e. A | ph } = (/) <-> A. y -. [ y / x ] ( x e. A /\ ph ) )
16	5, 7, 15	3bitr4ri 213	. 2 |- ( { x e. A | ph } = (/) <-> A. x -. ( x e. A /\ ph ) )
17	2, 3, 16	3bitr4ri 213	1 |- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1362   = wceq 1364   [wsb 1773   e. wcel 2164   {cab 2179   A.wral 2472   {crab 2476   (/)c0 3446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rab 2481  df-v 2762  df-dif 3155  df-nul 3447

This theorem is referenced by:  rabnc  3479  rabrsndc  3686  exmidsssnc  4232  ssfilem  6931  diffitest  6943  ssfirab  6990  ctssexmid  7209  exmidonfinlem  7253  iooidg  9975  icc0r  9992  fznlem  10107  ioo0  10328  ico0  10330  ioc0  10331  phiprmpw  12360  hashgcdeq  12377  unennn  12554  znnen  12555  fczpsrbag  14157