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

Theorem ssexd 4728
Description: A subclass of a set is a set. Deduction form of ssexg 4727. (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 4727 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
41, 2, 3syl2anc 690 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  Vcvv 3172  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553
This theorem is referenced by:  sselpwd  4729  opabbrex  6571  opabex2  6974  soex  6979  fex2  6991  fnwelem  7156  fnse  7158  extmptsuppeq  7183  f1imaen2g  7880  ordtypelem10  8292  oismo  8305  wofib  8310  wemapso  8316  wdom2d  8345  wdomd  8346  unxpwdom2  8353  cantnfle  8428  cantnflt  8429  cantnflt2  8430  cantnfp1lem2  8436  cantnfp1lem3  8437  cantnflem1b  8443  cantnflem1d  8445  cantnflem1  8446  cnfcomlem  8456  cnfcom  8457  cnfcom2lem  8458  cnfcom3lem  8460  acni2  8729  fin1a2lem12  9093  hsmexlem1  9108  zorn2lem4  9181  fpwwe2lem2  9310  fpwwe2lem5  9312  fpwwe2lem12  9319  fpwwe2  9321  fpwwelem  9323  canthwelem  9328  pwfseqlem4  9340  trclfv  13535  hashbcss  15492  strssd  15683  restid2  15860  divsfval  15976  mrieqv2d  16068  mrissmrcd  16069  mreexexlemd  16073  mreexexlem3d  16075  mreexexlem4d  16076  mreexexdOLD  16078  mreexdomd  16079  rescabs  16262  rescabs2  16263  resssetc  16511  resscatc  16524  estrres  16548  yonedalem1  16681  yonedalem21  16682  yonedalem3a  16683  yonedalem4c  16686  yonedalem22  16687  yonedalem3b  16688  yonedainv  16690  yonffthlem  16691  joinfval  16770  meetfval  16784  acsdomd  16950  gass  17503  pmtrfconj  17655  sylow2blem2  17805  dprdres  18196  dmdprdsplitlem  18205  pwssplit0  18825  pwssplit1  18826  pwssplit2  18827  pwssplit3  18828  opsrtoslem2  19252  evls1gsumadd  19456  evls1gsummul  19457  evl1gsummul  19491  frlmsplit2  19873  frlmsslss  19874  neiptoptop  20687  lpval  20695  neitr  20736  ordtbaslem  20744  ordtrest2  20760  cnrest2  20842  cnpresti  20844  cnprest  20845  cnprest2  20846  consuba  20975  consubclo  20979  uncon  20984  1stcelcls  21016  hausmapdom  21055  dissnref  21083  ptbasfi  21136  ptcls  21171  cnmpt2res  21232  qtopval2  21251  elqtop  21252  qtoprest  21272  ptuncnv  21362  ptunhmeo  21363  fsubbas  21423  elfm  21503  rnelfmlem  21508  rnelfm  21509  fmfnfmlem4  21513  flimclslem  21540  hauspwpwdom  21544  ptcmplem1  21608  cnextcn  21623  cnextfres1  21624  isust  21759  trust  21785  elutop  21789  restutop  21793  trcfilu  21850  cfiluweak  21851  psmetres2  21871  xmetres2  21917  fmcfil  22796  dvnf  23413  dvnbss  23414  dvaddf  23428  dvmulf  23429  dvcmulf  23431  dvcof  23434  ulmss  23872  perpln1  25323  perpln2  25324  isperp  25325  wlks  25813  trls  25832  resf1o  28699  crefi  29048  ordtrest2NEW  29103  lmlim  29127  esummono  29249  esumrnmpt2  29263  esumpinfval  29268  carsgmon  29509  carsggect  29513  bnj1413  30163  cvmliftmolem1  30323  fwddifval  31245  neibastop1  31330  neibastop2lem  31331  fnejoin1  31339  filnetlem3  31351  filnetlem4  31352  dissneqlem  32166  elrfi  36078  elrfirn2  36080  clcnvlem  36752  relexpss1d  36819  k0004lem2  37269  ixpssmapc  38072  restuni4  38139  wessf1ornlem  38169  unirnmap  38198  inmap  38199  difmapsn  38202  unirnmapsn  38204  ssmapsn  38206  limsupre  38512  icccncfext  38577  dvdivcncf  38621  dvnprodlem1  38640  dvnprodlem2  38641  ovolsplit  38685  stoweidlem31  38728  stoweidlem53  38750  stoweidlem57  38754  stoweidlem59  38756  etransclem46  38977  saliuncl  39022  salexct  39032  subsaluni  39058  fsumlesge0  39074  sge0f1o  39079  sge0iunmptlemfi  39110  sge0iunmptlemre  39112  meadjuni  39154  meadjiunlem  39162  omessle  39192  omecl  39197  isomenndlem  39224  caragencmpl  39229  ovnval2  39239  ovnval2b  39246  ovncvrrp  39258  ovncl  39261  hoidmvlelem2  39290  hoidmvlelem3  39291  ovncvr2  39305  ovnsubadd2lem  39339  ovnovollem3  39352  vonvolmbllem  39354  vonvolmbl  39355  issmfltle  39426  sssmf  39429  incsmf  39433  issmflelem  39435  issmfle  39436  smfconst  39440  issmfgtlem  39446  issmfgt  39447  smfaddlem2  39454  decsmf  39457  issmfgelem  39459  issmfge  39460  nsssmfmbflem  39468  smfpimioo  39476  smfresal  39477  smfmullem4  39483  smfpimbor1lem1  39487  smf2id  39490  1wlksfval  40813  wlksfval  40814
  Copyright terms: Public domain W3C validator