MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssexd Structured version   Visualization version   GIF version

Theorem ssexd 4939
Description: A subclass of a set is a set. Deduction form of ssexg 4938. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
ssexd.1 (𝜑𝐵𝐶)
ssexd.2 (𝜑𝐴𝐵)
Assertion
Ref Expression
ssexd (𝜑𝐴 ∈ V)

Proof of Theorem ssexd
StepHypRef Expression
1 ssexd.2 . 2 (𝜑𝐴𝐵)
2 ssexd.1 . 2 (𝜑𝐵𝐶)
3 ssexg 4938 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
41, 2, 3syl2anc 573 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  Vcvv 3351  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-ss 3737
This theorem is referenced by:  sselpwd  4941  opabbrex  6842  soex  7256  fex2  7268  opabex2  7376  fnwelem  7443  fnse  7445  extmptsuppeq  7470  f1imaen2g  8170  ordtypelem10  8588  oismo  8601  wofib  8606  wemapso  8612  wdom2d  8641  wdomd  8642  unxpwdom2  8649  cantnfle  8732  cantnflt  8733  cantnflt2  8734  cantnfp1lem2  8740  cantnfp1lem3  8741  cantnflem1b  8747  cantnflem1d  8749  cnfcom  8761  cnfcom2lem  8762  djuexALT  8948  acni2  9069  fin1a2lem12  9435  hsmexlem1  9450  zorn2lem4  9523  fpwwe2lem2  9656  fpwwe2lem5  9658  fpwwe2lem12  9665  fpwwe2  9667  fpwwelem  9669  canthwelem  9674  pwfseqlem4  9686  trclfv  13949  hashbcss  15915  strssd  16116  restid2  16299  divsfval  16415  mrieqv2d  16507  mrissmrcd  16508  mreexexlemd  16512  mreexexlem3d  16514  mreexexlem4d  16515  mreexdomd  16517  rescabs  16700  rescabs2  16701  resssetc  16949  resscatc  16962  estrresOLD  16986  estrres  16987  yonedalem1  17120  yonedalem21  17121  yonedalem3a  17122  yonedalem4c  17125  yonedalem22  17126  yonedalem3b  17127  yonedainv  17129  yonffthlem  17130  joinfval  17209  meetfval  17223  acsdomd  17389  gass  17941  pmtrfconj  18093  sylow2blem2  18243  dprdres  18635  dmdprdsplitlem  18644  pwssplit0  19271  pwssplit1  19272  pwssplit2  19273  pwssplit3  19274  opsrtoslem2  19700  evls1gsumadd  19904  evls1gsummul  19905  evl1gsummul  19939  frlmsplit2  20329  frlmsslss  20330  neiptoptop  21156  lpval  21164  neitr  21205  ordtbaslem  21213  ordtrest2  21229  cnrest2  21311  cnpresti  21313  cnprest  21314  cnprest2  21315  connsuba  21444  connsubclo  21448  unconn  21453  1stcelcls  21485  hausmapdom  21524  dissnref  21552  ptbasfi  21605  ptcls  21640  cnmpt2res  21701  qtopval2  21720  elqtop  21721  qtoprest  21741  ptuncnv  21831  ptunhmeo  21832  fsubbas  21891  elfm  21971  rnelfmlem  21976  rnelfm  21977  fmfnfmlem4  21981  flimclslem  22008  hauspwpwdom  22012  ptcmplem1  22076  cnextcn  22091  cnextfres1  22092  isust  22227  trust  22253  elutop  22257  restutop  22261  trcfilu  22318  cfiluweak  22319  psmetres2  22339  xmetres2  22386  fmcfil  23289  dvnf  23910  dvnbss  23911  dvaddf  23925  dvmulf  23926  dvcmulf  23928  dvcof  23931  ulmss  24371  perpln1  25826  perpln2  25827  isperp  25828  wksfval  26740  resf1o  29845  ordtrest2NEW  30309  lmlim  30333  esummono  30456  esumrnmpt2  30470  esumpinfval  30475  carsgmon  30716  carsggect  30720  reprval  31028  repr0  31029  reprsuc  31033  reprss  31035  reprinrn  31036  reprlt  31037  reprgt  31039  reprinfz1  31040  reprpmtf1o  31044  reprdifc  31045  bnj1413  31441  cvmliftmolem1  31601  nosupno  32186  sssslt1  32243  sssslt2  32244  fwddifval  32606  neibastop1  32691  neibastop2lem  32692  fnejoin1  32700  filnetlem3  32712  filnetlem4  32713  dissneqlem  33524  elrfi  37783  elrfirn2  37785  clcnvlem  38456  relexpss1d  38523  k0004lem2  38972  ixpssmapc  39764  restuni4  39825  wessf1ornlem  39891  unirnmap  39918  inmap  39919  difmapsn  39922  unirnmapsn  39924  ssmapsn  39926  limsupre  40391  limsuppnfdlem  40451  limsuppnflem  40460  limsupmnflem  40470  limsupre2lem  40474  liminfval4  40539  liminfval3  40540  icccncfext  40618  dvdivcncf  40660  dvnprodlem1  40679  dvnprodlem2  40680  ovolsplit  40722  stoweidlem31  40765  stoweidlem53  40787  stoweidlem57  40791  stoweidlem59  40793  etransclem46  41014  saliuncl  41059  salexct  41069  subsaluni  41095  fsumlesge0  41111  sge0f1o  41116  sge0iunmptlemfi  41147  sge0iunmptlemre  41149  meadjuni  41191  meadjiunlem  41199  omessle  41232  omecl  41237  isomenndlem  41264  caragencmpl  41269  ovnval2  41279  ovnval2b  41286  ovncvrrp  41298  ovncl  41301  hoidmvlelem2  41330  hoidmvlelem3  41331  ovncvr2  41345  ovnsubadd2lem  41379  ovnovollem3  41392  vonvolmbllem  41394  vonvolmbl  41395  sssmf  41467  incsmf  41471  issmflelem  41473  issmfle  41474  smfconst  41478  issmfgtlem  41484  issmfgt  41485  smfaddlem2  41492  decsmf  41495  issmfgelem  41497  issmfge  41498  nsssmfmbflem  41506  smfpimioo  41514  smfresal  41515  smfmullem4  41521  smfpimbor1lem1  41525  smf2id  41528  upwlksfval  42244
  Copyright terms: Public domain W3C validator