Theorem ssrab2 2131

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 1652	. 2 |- {x e. A | ph} = {x | (x e. A /\ ph)}
2		ssab2 2130	. 2 |- {x | (x e. A /\ ph)} (_ A
3	1, 2	eqsstr 2091	1 |- {x e. A | ph} (_ A

Syntax hints:   /\ wa 223   e. wcel 958  {cab 1463  {crab 1648   (_ wss 2047

This theorem is referenced by:  rabexg 2724  rabsnt 2894  onminsb 3009  onminesb 3010  onintrab 3013  onnminsb 3016  tfis 3127  ssimaex 3768  canth 3907  oawordeulem 4188  tz9.12lem1 4659  tz9.12lem3 4661  rankon 4671  rankr1 4674  rankeq0 4696  cplem1 4720  hta 4728  ac6lem 4754  kmlem1 4765  zorn2lem1 4788  zorn2lem3 4790  zorn2lem4 4791  zorn2lem5 4792  oncardval 4819  oncardon 4820  oncardid 4821  cardon 4827  cardid 4828  ondomon 4856  cardmin 4860  alephval2 4902  nnind 5937  lbcl 6046  infm3 6054  infmrcl 6069  uzwo4OLD 6210  uzwo5OLD 6211  flval3t 6239  rpret 6284  om2uzlt 6298  om2uzlt2 6299  om2uzf1o 6301  iccf 6401  uzssz 6430  nnwos 6460  sqrlem6 6678  seq1ublem 6911  seq1ub 6912  caucvglem2 7158  ivthlem4 7284  ivthlem5 7285  ivthlem7 7287  ivthlem9 7289  infpn2 7509  clscld 7683  ntropn 7684  neiint 7719  neips 7727  cncnplem4 7777  blf 7844  blssm 7850  pilem2 8672  pilem3 8673  shftefif1olem 8741  explogt 8772  ocsh 9156  projlem8 9193  shscl 9281  ococint 9297  spanclt 9304  hsupclt 9307  chsupid 9311  shsumval2 9360  specclt 9825  elnlfn2t 9853  nmcopexlem4 9954  nmcfnexlem4 9983  nlelsh 9993  hmopidmch 10079  hmopidmpj 10080  atssch 10270  hatomistic 10289  chpssat 10290  ump 10459

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-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-rab 1652  df-in 2051  df-ss 2053

Copyright terms: Public domain