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

Theorem ssexd 5220
Description: A subclass of a set is a set. Deduction form of ssexg 5219. (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 5219 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
41, 2, 3syl2anc 584 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3495  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-in 3942  df-ss 3951
This theorem is referenced by:  sselpwd  5222  opabbrex  7196  soex  7614  fex2  7626  funexw  7644  opabex2  7746  fnwelem  7816  fnse  7818  extmptsuppeq  7845  f1imaen2g  8559  ordtypelem10  8980  oismo  8993  wofib  8998  wemapso  9004  wdom2d  9033  wdomd  9034  unxpwdom2  9041  djuexALT  9340  acni2  9461  fin1a2lem12  9822  hsmexlem1  9837  zorn2lem4  9910  fpwwe2lem2  10043  fpwwe2lem5  10045  fpwwe2lem12  10052  fpwwe2  10054  fpwwelem  10056  canthwelem  10061  pwfseqlem4  10073  trclfv  14350  hashbcss  16330  strssd  16523  restid2  16694  divsfval  16810  mrieqv2d  16900  mrissmrcd  16901  mreexexlemd  16905  mreexexlem3d  16907  mreexexlem4d  16908  mreexdomd  16910  rescabs  17093  rescabs2  17094  resssetc  17342  resscatc  17355  estrres  17379  yonedalem1  17512  yonedalem21  17513  yonedalem3a  17514  yonedalem4c  17517  yonedalem22  17518  yonedalem3b  17519  yonedainv  17521  yonffthlem  17522  joinfval  17601  meetfval  17615  acsdomd  17781  gass  18371  pmtrfconj  18525  sylow2blem2  18677  dprdres  19081  dmdprdsplitlem  19090  primefld  19515  pwssplit0  19761  pwssplit1  19762  pwssplit2  19763  pwssplit3  19764  opsrtoslem2  20195  evlsgsumadd  20234  evlsgsummul  20235  evls1gsumadd  20417  evls1gsummul  20418  evl1gsummul  20453  frlmsplit2  20847  frlmsslss  20848  neiptoptop  21669  lpval  21677  neitr  21718  ordtbaslem  21726  ordtrest2  21742  cnrest2  21824  cnpresti  21826  cnprest  21827  cnprest2  21828  connsuba  21958  connsubclo  21962  unconn  21967  1stcelcls  21999  hausmapdom  22038  dissnref  22066  ptbasfi  22119  ptcls  22154  cnmpt2res  22215  qtopval2  22234  elqtop  22235  qtoprest  22255  ptuncnv  22345  ptunhmeo  22346  fsubbas  22405  elfm  22485  rnelfmlem  22490  rnelfm  22491  fmfnfmlem4  22495  flimclslem  22522  hauspwpwdom  22526  ptcmplem1  22590  cnextcn  22605  cnextfres1  22606  isust  22741  trust  22767  elutop  22771  restutop  22775  trcfilu  22832  cfiluweak  22833  psmetres2  22853  xmetres2  22900  fmcfil  23804  dvaddf  24468  dvmulf  24469  dvcmulf  24471  dvcof  24474  ulmss  24914  perpln1  26424  perpln2  26425  isperp  26426  wksfval  27319  fnpreimac  30345  resf1o  30393  cycpmco2lem5  30700  islinds5  30860  ellspds  30861  lbsdiflsp0  30922  ordtrest2NEW  31066  lmlim  31090  esummono  31213  esumrnmpt2  31227  esumpinfval  31232  elcarsg  31463  carsgmon  31472  carsggect  31476  reprval  31781  repr0  31782  reprsuc  31786  reprss  31788  reprinrn  31789  reprlt  31790  reprgt  31792  reprinfz1  31793  reprpmtf1o  31797  reprdifc  31798  bnj1413  32205  cvmliftmolem1  32426  satf0suclem  32520  nosupno  33101  sssslt1  33158  sssslt2  33159  fwddifval  33521  neibastop1  33605  neibastop2lem  33606  fnejoin1  33614  filnetlem3  33626  filnetlem4  33627  bj-imdirval2  34366  bj-imdirval3  34367  dissneqlem  34504  selvval2lemn  39015  selvval2lem4  39016  selvval2lem5  39017  selvcl  39018  elrfi  39171  elrfirn2  39173  clcnvlem  39863  relexpss1d  39930  k0004lem2  40378  ixpssmapc  41216  restuni4  41268  wessf1ornlem  41325  unirnmap  41351  inmap  41352  difmapsn  41355  unirnmapsn  41357  ssmapsn  41359  limsupre  41802  limsuppnfdlem  41862  limsuppnflem  41871  limsupmnflem  41881  limsupre2lem  41885  liminfval4  41950  liminfval3  41951  icccncfext  42050  dvdivcncf  42092  dvnprodlem1  42111  dvnprodlem2  42112  ovolsplit  42154  stoweidlem31  42197  stoweidlem53  42219  stoweidlem57  42223  stoweidlem59  42225  etransclem46  42446  saliuncl  42488  salexct  42498  subsaluni  42524  fsumlesge0  42540  sge0f1o  42545  sge0iunmptlemfi  42576  sge0iunmptlemre  42578  meadjuni  42620  meadjiunlem  42628  omessle  42661  omecl  42666  isomenndlem  42693  caragencmpl  42698  ovnval2  42708  ovnval2b  42715  ovncvrrp  42727  ovncl  42730  hoidmvlelem2  42759  hoidmvlelem3  42760  ovncvr2  42774  ovnsubadd2lem  42808  ovnovollem3  42821  vonvolmbllem  42823  vonvolmbl  42824  sssmf  42896  incsmf  42900  issmflelem  42902  issmfle  42903  smfconst  42907  issmfgtlem  42913  issmfgt  42914  smfaddlem2  42921  decsmf  42924  issmfgelem  42926  issmfge  42927  nsssmfmbflem  42935  smfpimioo  42943  smfresal  42944  smfmullem4  42950  smfpimbor1lem1  42954  smf2id  42957  upwlksfval  43857
  Copyright terms: Public domain W3C validator