Theorem rabn0 1716

Description: Non-empty restricted class abstraction.

Assertion

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

Proof of Theorem rabn0

Step	Hyp	Ref	Expression
1		abn0 1715	. 2 |- (-. {x | (x e. A /\ ph)} = (/) <-> E.x(x e. A /\ ph))
2		df-rab 1208	. . . 4 |- {x e. A | ph} = {x | (x e. A /\ ph)}
3	2	cleq1i 1108	. . 3 |- ({x e. A | ph} = (/) <-> {x | (x e. A /\ ph)} = (/))
4	3	negbii 162	. 2 |- (-. {x e. A | ph} = (/) <-> -. {x | (x e. A /\ ph)} = (/))
5		df-rex 1206	. 2 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
6	1, 4, 5	3bitr4 158	1 |- (-. {x e. A | ph} = (/) <-> E.x e. A ph)

Syntax hints:  -. wn 1   <-> wb 127   /\ wa 196  E.wex 678  {cab 1090   = wceq 1091   e. wcel 1092  E.wrex 1202  {crab 1204  (/)c0 1707

This theorem is referenced by:  rab0 1718  class2set 1747  exss 1881  onminsb 2264  onminesb 2265  tz9.12lem3 3505  rankval 3512  rankon 3515  rankr1 3518  scott0 3542  karden 3551  ac6lem 3575  kmlem3 3582  oncardval 3626  nnwos 4610  uzwo3lem1 4614  ococint 5298  spanclt 5305  shsumval2 5361

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-rab 1208  df-v 1349  df-dif 1489  df-nul 1708

metamath.org