ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssrab2 GIF version

Theorem ssrab2 3150
Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
ssrab2 {𝑥𝐴𝜑} ⊆ 𝐴
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrab2
StepHypRef Expression
1 df-rab 2400 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 ssab2 3149 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
31, 2eqsstri 3097 1 {𝑥𝐴𝜑} ⊆ 𝐴
Colors of variables: wff set class
Syntax hints:  wa 103  wcel 1463  {cab 2101  {crab 2395  wss 3039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rab 2400  df-in 3045  df-ss 3052
This theorem is referenced by:  ssrabeq  3151  rabexg  4039  pwnss  4051  undifexmid  4085  exmidexmid  4088  exmidsssnc  4094  onintrab2im  4402  ordtriexmidlem  4403  ontr2exmid  4408  ordtri2or2exmidlem  4409  onsucsssucexmid  4410  onsucelsucexmidlem  4412  tfis  4465  nnregexmid  4502  dmmptss  5003  ssimaex  5448  f1oresrab  5551  riotacl  5710  pmvalg  6519  ssfiexmid  6736  domfiexmid  6738  ctssdccl  6962  ctssexmid  6990  genpelxp  7283  ltexprlempr  7380  cauappcvgprlemcl  7425  cauappcvgprlemladd  7430  caucvgprlemcl  7448  caucvgprprlemcl  7476  suplocexprlemex  7494  uzf  9281  supminfex  9344  rpre  9399  ixxf  9632  fzf  9745  expcl2lemap  10256  expclzaplem  10268  expge0  10280  expge1  10281  dvdsflip  11456  infssuzex  11549  infssuzcldc  11551  gcddvds  11559  lcmn0cl  11656  phicl2  11796  phimullem  11807  ennnfonelemg  11822  ennnfonelemh  11823  ctiunctlemuom  11855  epttop  12165  neipsm  12229  cnpfval  12270  blfvalps  12460  blfps  12484  blf  12485  divcnap  12630  cdivcncfap  12662  cnopnap  12669  ivthinclemex  12695  limcdifap  12706  dvfgg  12732  dvidlemap  12735  dvcnp2cntop  12738  dvaddxxbr  12740  dvmulxxbr  12741  dvcoapbr  12746  dvrecap  12752  bdrabexg  12938  subctctexmid  13030
  Copyright terms: Public domain W3C validator