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

Theorem ssexd 5219
Description: A subclass of a set is a set. Deduction form of ssexg 5218. (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 5218 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
41, 2, 3syl2anc 586 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3493  wss 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-in 3941  df-ss 3950
This theorem is referenced by:  sselpwd  5221  opabbrex  7199  soex  7618  fex2  7630  funexw  7645  opabex2  7747  fnwelem  7817  fnse  7819  extmptsuppeq  7846  f1imaen2g  8562  ordtypelem10  8983  oismo  8996  wofib  9001  wemapso  9007  wdom2d  9036  wdomd  9037  unxpwdom2  9044  djuexALT  9343  acni2  9464  fin1a2lem12  9825  hsmexlem1  9840  zorn2lem4  9913  fpwwe2lem2  10046  fpwwe2lem5  10048  fpwwe2lem12  10055  fpwwe2  10057  fpwwelem  10059  canthwelem  10064  pwfseqlem4  10076  trclfv  14352  hashbcss  16332  strssd  16525  restid2  16696  divsfval  16812  mrieqv2d  16902  mrissmrcd  16903  mreexexlemd  16907  mreexexlem3d  16909  mreexexlem4d  16910  mreexdomd  16912  rescabs  17095  rescabs2  17096  resssetc  17344  resscatc  17357  estrres  17381  yonedalem1  17514  yonedalem21  17515  yonedalem3a  17516  yonedalem4c  17519  yonedalem22  17520  yonedalem3b  17521  yonedainv  17523  yonffthlem  17524  joinfval  17603  meetfval  17617  acsdomd  17783  gass  18423  permsetex  18490  pmtrfconj  18586  sylow2blem2  18738  dprdres  19142  dmdprdsplitlem  19151  primefld  19576  pwssplit0  19822  pwssplit1  19823  pwssplit2  19824  pwssplit3  19825  opsrtoslem2  20257  evlsgsumadd  20296  evlsgsummul  20297  evls1gsumadd  20479  evls1gsummul  20480  evl1gsummul  20515  frlmsplit2  20909  frlmsslss  20910  neiptoptop  21731  lpval  21739  neitr  21780  ordtbaslem  21788  ordtrest2  21804  cnrest2  21886  cnpresti  21888  cnprest  21889  cnprest2  21890  connsuba  22020  connsubclo  22024  unconn  22029  1stcelcls  22061  hausmapdom  22100  dissnref  22128  ptbasfi  22181  ptcls  22216  cnmpt2res  22277  qtopval2  22296  elqtop  22297  qtoprest  22317  ptuncnv  22407  ptunhmeo  22408  fsubbas  22467  elfm  22547  rnelfmlem  22552  rnelfm  22553  fmfnfmlem4  22557  flimclslem  22584  hauspwpwdom  22588  ptcmplem1  22652  cnextcn  22667  cnextfres1  22668  isust  22804  trust  22830  elutop  22834  restutop  22838  trcfilu  22895  cfiluweak  22896  psmetres2  22916  xmetres2  22963  fmcfil  23867  dvaddf  24531  dvmulf  24532  dvcmulf  24534  dvcof  24537  ulmss  24977  perpln1  26488  perpln2  26489  isperp  26490  wksfval  27383  fnpreimac  30408  resf1o  30458  cycpmco2lem5  30765  islinds5  30925  ellspds  30926  lbsdiflsp0  31010  ordtrest2NEW  31154  lmlim  31178  esummono  31301  esumrnmpt2  31315  esumpinfval  31320  elcarsg  31551  carsgmon  31560  carsggect  31564  reprval  31869  repr0  31870  reprsuc  31874  reprss  31876  reprinrn  31877  reprlt  31878  reprgt  31880  reprinfz1  31881  reprpmtf1o  31885  reprdifc  31886  bnj1413  32295  cvmliftmolem1  32516  satf0suclem  32610  nosupno  33191  sssslt1  33248  sssslt2  33249  fwddifval  33611  neibastop1  33695  neibastop2lem  33696  fnejoin1  33704  filnetlem3  33716  filnetlem4  33717  bj-imdirval2  34460  bj-imdirval3  34461  dissneqlem  34608  selvval2lemn  39120  selvval2lem4  39121  selvval2lem5  39122  selvcl  39123  elrfi  39276  elrfirn2  39278  clcnvlem  39968  relexpss1d  40035  k0004lem2  40483  ixpssmapc  41321  restuni4  41372  wessf1ornlem  41429  unirnmap  41455  inmap  41456  difmapsn  41459  unirnmapsn  41461  ssmapsn  41463  limsupre  41906  limsuppnfdlem  41966  limsuppnflem  41975  limsupmnflem  41985  limsupre2lem  41989  liminfval4  42054  liminfval3  42055  icccncfext  42154  dvdivcncf  42196  dvnprodlem1  42215  dvnprodlem2  42216  ovolsplit  42258  stoweidlem31  42301  stoweidlem53  42323  stoweidlem57  42327  stoweidlem59  42329  etransclem46  42550  saliuncl  42592  salexct  42602  subsaluni  42628  fsumlesge0  42644  sge0f1o  42649  sge0iunmptlemfi  42680  sge0iunmptlemre  42682  meadjuni  42724  meadjiunlem  42732  omessle  42765  omecl  42770  isomenndlem  42797  caragencmpl  42802  ovnval2  42812  ovnval2b  42819  ovncvrrp  42831  ovncl  42834  hoidmvlelem2  42863  hoidmvlelem3  42864  ovncvr2  42878  ovnsubadd2lem  42912  ovnovollem3  42925  vonvolmbllem  42927  vonvolmbl  42928  sssmf  43000  incsmf  43004  issmflelem  43006  issmfle  43007  smfconst  43011  issmfgtlem  43017  issmfgt  43018  smfaddlem2  43025  decsmf  43028  issmfgelem  43030  issmfge  43031  nsssmfmbflem  43039  smfpimioo  43047  smfresal  43048  smfmullem4  43054  smfpimbor1lem1  43058  smf2id  43061  upwlksfval  43995
  Copyright terms: Public domain W3C validator