Theorem rabn0 2292

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 2290	. 2 |- ({x | (x e. A /\ ph)} =/= (/) <-> E.x(x e. A /\ ph))
2		df-rab 1652	. . 3 |- {x e. A | ph} = {x | (x e. A /\ ph)}
3	2	neeq1i 1592	. 2 |- ({x e. A | ph} =/= (/) <-> {x | (x e. A /\ ph)} =/= (/))
4		df-rex 1650	. 2 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
5	1, 3, 4	3bitr4 183	1 |- ({x e. A | ph} =/= (/) <-> E.x e. A ph)

Syntax hints:   <-> wb 146   /\ wa 223   e. wcel 958  E.wex 980  {cab 1463   =/= wne 1585  E.wrex 1646  {crab 1648  (/)c0 2280

This theorem is referenced by:  rab0 2293  class2set 2734  exss 2769  onminsb 3009  onminesb 3010  tz9.12lem3 4661  rankval 4668  rankon 4671  rankr1 4674  scott0 4717  karden 4726  ac6lem 4754  kmlem3 4767  oncardval 4819  infm3 6054  uzwo3lem1 6216  ioo0t 6368  nnwos 6460  spwval3 8654  spwnex3 8655  ococint 9297  spanclt 9304  shsumval2 9360  nmcopexlem4 9954  nmcfnexlem4 9983

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-rex 1650  df-rab 1652  df-v 1812  df-dif 2049  df-nul 2281

Copyright terms: Public domain