Theorem ssrab2 2183

Description: Subclass relation for a restricted class.

Assertion

Ref	Expression
ssrab2	|- {x e. A | ph} (_ A

Distinct variable group:   x,A

Proof of Theorem ssrab2

Step	Hyp	Ref	Expression
1		df-rab 1698	. 2 |- {x e. A | ph} = {x | (x e. A /\ ph)}
2		ssab2 2182	. 2 |- {x | (x e. A /\ ph)} (_ A
3	1, 2	eqsstri 2143	1 |- {x e. A | ph} (_ A

Syntax hints:   /\ wa 221   e. wcel 994  {cab 1505  {crab 1694   (_ wss 2099

This theorem is referenced by:  rabexg 2798  rabsnt 3117  onminsb 3155  onminesb 3156  onintrab 3158  onnminsb 3161  tfis 3208  ssimaex 3879  canth 4205  oawordeulem 4324  tz9.12lem1 4805  tz9.12lem3 4807  rankon 4817  rankr1 4820  rankeq0 4842  cplem1 4866  hta 4874  ac6lem 4900  kmlem1 4911  zorn2lem1 4934  zorn2lem3 4936  zorn2lem4 4937  zorn2lem5 4938  oncardval 4965  oncardon 4966  oncardid 4967  cardon 4974  cardid 4975  ondomon 5006  cardmin 5010  alephval2 5052  nnind 6082  rpre 6195  lbcl 6214  infm3 6222  infmrcl 6237  uzwo4OLD 6381  uzwo5OLD 6382  flval3 6438  iccf 6528  uzssz 6557  nnwos 6587  om2uzlti 6661  om2uzlt2i 6662  om2uzf1oi 6664  sqrlem6 6879  seq1ublem 7114  seq1ubi 7115  caucvglem2 7361  ivthlem4 7489  ivthlem5 7490  ivthlem7 7492  ivthlem9 7494  infpn2 7721  clscld 7893  ntropn 7894  neiint 7929  neips 7937  cncnplem4 7987  blf 8054  blssm 8060  pilem2 8939  pilem3 8940  shftefif1olem 9013  explog 9044  ocsh 9432  projlem8 9469  shscli 9557  ococin 9573  spancl 9580  hsupcl 9583  chsupid 9587  shsumval2i 9636  speccl 10105  elnlfn2 10133  nmcopexlem4 10233  nmcfnexlem4 10262  nlelshi 10272  hmopidmchi 10359  hmopidmpji 10360  atssch 10551  hatomistici 10570  chpssati 10571  ump 10743  finminlem 11418  ordtypelem1 11427  ordtypelem3 11429  ordtypelem4 11430  ordtypelem6 11432  ordtypelem7 11433  hartog 11436  compsublem 11487  hscptsscld 11491  alexsub 11500  2ndc1stc 11538  isfne3 11543  fnessref 11564  finptfin 11568  finlocfin 11570  locfincomp 11575  indexa 11845  sstotbnd 11992  totbndss 11993  totbndbnd 12000

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-rab 1698  df-in 2103  df-ss 2105

Copyright terms: Public domain