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

Theorem ssexd 4796
Description: A subclass of a set is a set. Deduction form of ssexg 4795. (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 4795 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
41, 2, 3syl2anc 692 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  Vcvv 3195  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ss 3581
This theorem is referenced by:  sselpwd  4798  opabbrex  6680  soex  7094  fex2  7106  opabex2  7212  fnwelem  7277  fnse  7279  extmptsuppeq  7304  f1imaen2g  8002  ordtypelem10  8417  oismo  8430  wofib  8435  wemapso  8441  wdom2d  8470  wdomd  8471  unxpwdom2  8478  cantnfle  8553  cantnflt  8554  cantnflt2  8555  cantnfp1lem2  8561  cantnfp1lem3  8562  cantnflem1b  8568  cantnflem1d  8570  cnfcom  8582  cnfcom2lem  8583  acni2  8854  fin1a2lem12  9218  hsmexlem1  9233  zorn2lem4  9306  fpwwe2lem2  9439  fpwwe2lem5  9441  fpwwe2lem12  9448  fpwwe2  9450  fpwwelem  9452  canthwelem  9457  pwfseqlem4  9469  trclfv  13722  hashbcss  15689  strssd  15890  restid2  16072  divsfval  16188  mrieqv2d  16280  mrissmrcd  16281  mreexexlemd  16285  mreexexlem3d  16287  mreexexlem4d  16288  mreexexdOLD  16290  mreexdomd  16291  rescabs  16474  rescabs2  16475  resssetc  16723  resscatc  16736  estrres  16760  yonedalem1  16893  yonedalem21  16894  yonedalem3a  16895  yonedalem4c  16898  yonedalem22  16899  yonedalem3b  16900  yonedainv  16902  yonffthlem  16903  joinfval  16982  meetfval  16996  acsdomd  17162  gass  17715  pmtrfconj  17867  sylow2blem2  18017  dprdres  18408  dmdprdsplitlem  18417  pwssplit0  19039  pwssplit1  19040  pwssplit2  19041  pwssplit3  19042  opsrtoslem2  19466  evls1gsumadd  19670  evls1gsummul  19671  evl1gsummul  19705  frlmsplit2  20093  frlmsslss  20094  neiptoptop  20916  lpval  20924  neitr  20965  ordtbaslem  20973  ordtrest2  20989  cnrest2  21071  cnpresti  21073  cnprest  21074  cnprest2  21075  connsuba  21204  connsubclo  21208  unconn  21213  1stcelcls  21245  hausmapdom  21284  dissnref  21312  ptbasfi  21365  ptcls  21400  cnmpt2res  21461  qtopval2  21480  elqtop  21481  qtoprest  21501  ptuncnv  21591  ptunhmeo  21592  fsubbas  21652  elfm  21732  rnelfmlem  21737  rnelfm  21738  fmfnfmlem4  21742  flimclslem  21769  hauspwpwdom  21773  ptcmplem1  21837  cnextcn  21852  cnextfres1  21853  isust  21988  trust  22014  elutop  22018  restutop  22022  trcfilu  22079  cfiluweak  22080  psmetres2  22100  xmetres2  22147  fmcfil  23051  dvnf  23671  dvnbss  23672  dvaddf  23686  dvmulf  23687  dvcmulf  23689  dvcof  23692  ulmss  24132  perpln1  25586  perpln2  25587  isperp  25588  wksfval  26486  resf1o  29479  ordtrest2NEW  29943  lmlim  29967  esummono  30090  esumrnmpt2  30104  esumpinfval  30109  carsgmon  30350  carsggect  30354  reprval  30662  repr0  30663  reprsuc  30667  reprss  30669  reprinrn  30670  reprlt  30671  reprgt  30673  reprinfz1  30674  reprpmtf1o  30678  reprdifc  30679  bnj1413  31077  cvmliftmolem1  31237  nosupno  31823  sssslt1  31880  sssslt2  31881  fwddifval  32244  neibastop1  32329  neibastop2lem  32330  fnejoin1  32338  filnetlem3  32350  filnetlem4  32351  dissneqlem  33158  elrfi  37076  elrfirn2  37078  clcnvlem  37749  relexpss1d  37816  k0004lem2  38266  ixpssmapc  39063  restuni4  39124  wessf1ornlem  39187  unirnmap  39216  inmap  39217  difmapsn  39220  unirnmapsn  39222  ssmapsn  39224  limsupre  39673  limsuppnfdlem  39733  limsuppnflem  39742  limsupmnflem  39752  limsupre2lem  39756  liminfval4  39815  liminfval3  39816  icccncfext  39863  dvdivcncf  39905  dvnprodlem1  39924  dvnprodlem2  39925  ovolsplit  39968  stoweidlem31  40011  stoweidlem53  40033  stoweidlem57  40037  stoweidlem59  40039  etransclem46  40260  saliuncl  40305  salexct  40315  subsaluni  40341  fsumlesge0  40357  sge0f1o  40362  sge0iunmptlemfi  40393  sge0iunmptlemre  40395  meadjuni  40437  meadjiunlem  40445  omessle  40475  omecl  40480  isomenndlem  40507  caragencmpl  40512  ovnval2  40522  ovnval2b  40529  ovncvrrp  40541  ovncl  40544  hoidmvlelem2  40573  hoidmvlelem3  40574  ovncvr2  40588  ovnsubadd2lem  40622  ovnovollem3  40635  vonvolmbllem  40637  vonvolmbl  40638  sssmf  40710  incsmf  40714  issmflelem  40716  issmfle  40717  smfconst  40721  issmfgtlem  40727  issmfgt  40728  smfaddlem2  40735  decsmf  40738  issmfgelem  40740  issmfge  40741  nsssmfmbflem  40749  smfpimioo  40757  smfresal  40758  smfmullem4  40764  smfpimbor1lem1  40768  smf2id  40771  upwlksfval  41481
  Copyright terms: Public domain W3C validator