Theorem ssrab2 2121

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

Syntax hints:   /\ wa 223   e. wcel 955  {cab 1456  {crab 1640   (_ wss 2037

This theorem is referenced by:  rabexg 2714  rabsnt 2884  onminsb 2999  onminesb 3000  onintrab 3003  onnminsb 3006  tfis 3117  ssimaex 3753  canth 3892  oawordeulem 4172  tz9.12lem1 4631  tz9.12lem3 4633  rankon 4643  rankr1 4646  rankeq0 4668  cplem1 4692  hta 4700  ac6lem 4726  kmlem1 4737  zorn2lem1 4760  zorn2lem3 4762  zorn2lem4 4763  zorn2lem5 4764  oncardval 4791  oncardon 4792  oncardid 4793  cardon 4799  cardid 4800  ondomon 4828  cardmin 4832  alephval2 4874  nnind 5885  lbcl 5993  infm3 6001  infmrcl 6016  uzwo4OLD 6158  uzwo5OLD 6159  flval3t 6182  rpret 6222  om2uzlt 6235  om2uzlt2 6236  om2uzf1o 6238  iccf 6334  uzssz 6362  nnwos 6392  sqrlem6 6608  seq1ublem 6848  seq1ub 6849  caucvglem2 7094  ivthlem4 7219  ivthlem5 7220  ivthlem7 7222  ivthlem9 7224  ivthlem4OLD 7228  ivthlem5OLD 7229  ivthlem7OLD 7231  infpn2 7452  clscld 7625  ntropn 7626  neiint 7660  neips 7668  cncnplem4 7716  blf 7784  blssm 7790  pilem2 8591  pilem3 8592  circgrpOLD 8658  shftefif1olem 8661  shftefif1olemOLD 8662  explogt 8694  ocsh 9072  projlem8 9109  shscl 9196  ococint 9212  spanclt 9219  hsupclt 9222  chsupid 9226  shsumval2 9275  specclt 9742  elnlfn2t 9769  nmcopexlem4 9869  nmcfnexlem4 9898  nlelsh 9908  hmopidmch 9990  hmopidmpj 9991  atssch 10178  hatomistic 10197  chpssat 10198  ump 10355

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-rab 1644  df-in 2041  df-ss 2043

Copyright terms: Public domain