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

Theorem ssexd 4994
Description: A subclass of a set is a set. Deduction form of ssexg 4993. (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 4993 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
41, 2, 3syl2anc 575 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  Vcvv 3387  wss 3763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-in 3770  df-ss 3777
This theorem is referenced by:  sselpwd  4996  opabbrex  6919  soex  7333  fex2  7345  opabex2  7453  fnwelem  7520  fnse  7522  extmptsuppeq  7547  f1imaen2g  8247  ordtypelem10  8665  oismo  8678  wofib  8683  wemapso  8689  wdom2d  8718  wdomd  8719  unxpwdom2  8726  cantnfle  8809  cantnflt  8810  cantnflt2  8811  cantnfp1lem2  8817  cantnfp1lem3  8818  cantnflem1b  8824  cantnflem1d  8826  cnfcom  8838  cnfcom2lem  8839  djuexALT  9025  acni2  9146  fin1a2lem12  9512  hsmexlem1  9527  zorn2lem4  9600  fpwwe2lem2  9733  fpwwe2lem5  9735  fpwwe2lem12  9742  fpwwe2  9744  fpwwelem  9746  canthwelem  9751  pwfseqlem4  9763  trclfv  13958  hashbcss  15919  strssd  16114  restid2  16290  divsfval  16406  mrieqv2d  16498  mrissmrcd  16499  mreexexlemd  16503  mreexexlem3d  16505  mreexexlem4d  16506  mreexdomd  16508  rescabs  16691  rescabs2  16692  resssetc  16940  resscatc  16953  estrresOLD  16977  estrres  16978  yonedalem1  17111  yonedalem21  17112  yonedalem3a  17113  yonedalem4c  17116  yonedalem22  17117  yonedalem3b  17118  yonedainv  17120  yonffthlem  17121  joinfval  17200  meetfval  17214  acsdomd  17380  gass  17929  pmtrfconj  18081  sylow2blem2  18231  dprdres  18623  dmdprdsplitlem  18632  pwssplit0  19259  pwssplit1  19260  pwssplit2  19261  pwssplit3  19262  opsrtoslem2  19687  evls1gsumadd  19891  evls1gsummul  19892  evl1gsummul  19926  frlmsplit2  20316  frlmsslss  20317  neiptoptop  21143  lpval  21151  neitr  21192  ordtbaslem  21200  ordtrest2  21216  cnrest2  21298  cnpresti  21300  cnprest  21301  cnprest2  21302  connsuba  21431  connsubclo  21435  unconn  21440  1stcelcls  21472  hausmapdom  21511  dissnref  21539  ptbasfi  21592  ptcls  21627  cnmpt2res  21688  qtopval2  21707  elqtop  21708  qtoprest  21728  ptuncnv  21818  ptunhmeo  21819  fsubbas  21878  elfm  21958  rnelfmlem  21963  rnelfm  21964  fmfnfmlem4  21968  flimclslem  21995  hauspwpwdom  21999  ptcmplem1  22063  cnextcn  22078  cnextfres1  22079  isust  22214  trust  22240  elutop  22244  restutop  22248  trcfilu  22305  cfiluweak  22306  psmetres2  22326  xmetres2  22373  fmcfil  23276  dvnf  23898  dvnbss  23899  dvaddf  23913  dvmulf  23914  dvcmulf  23916  dvcof  23919  ulmss  24359  perpln1  25813  perpln2  25814  isperp  25815  wksfval  26727  resf1o  29826  ordtrest2NEW  30288  lmlim  30312  esummono  30435  esumrnmpt2  30449  esumpinfval  30454  carsgmon  30695  carsggect  30699  reprval  31007  repr0  31008  reprsuc  31012  reprss  31014  reprinrn  31015  reprlt  31016  reprgt  31018  reprinfz1  31019  reprpmtf1o  31023  reprdifc  31024  bnj1413  31420  cvmliftmolem1  31580  nosupno  32164  sssslt1  32221  sssslt2  32222  fwddifval  32584  neibastop1  32669  neibastop2lem  32670  fnejoin1  32678  filnetlem3  32690  filnetlem4  32691  dissneqlem  33498  elrfi  37753  elrfirn2  37755  clcnvlem  38424  relexpss1d  38491  k0004lem2  38940  ixpssmapc  39730  restuni4  39790  wessf1ornlem  39854  unirnmap  39881  inmap  39882  difmapsn  39885  unirnmapsn  39887  ssmapsn  39889  limsupre  40347  limsuppnfdlem  40407  limsuppnflem  40416  limsupmnflem  40426  limsupre2lem  40430  liminfval4  40495  liminfval3  40496  icccncfext  40574  dvdivcncf  40616  dvnprodlem1  40635  dvnprodlem2  40636  ovolsplit  40678  stoweidlem31  40721  stoweidlem53  40743  stoweidlem57  40747  stoweidlem59  40749  etransclem46  40970  saliuncl  41015  salexct  41025  subsaluni  41051  fsumlesge0  41067  sge0f1o  41072  sge0iunmptlemfi  41103  sge0iunmptlemre  41105  meadjuni  41147  meadjiunlem  41155  omessle  41188  omecl  41193  isomenndlem  41220  caragencmpl  41225  ovnval2  41235  ovnval2b  41242  ovncvrrp  41254  ovncl  41257  hoidmvlelem2  41286  hoidmvlelem3  41287  ovncvr2  41301  ovnsubadd2lem  41335  ovnovollem3  41348  vonvolmbllem  41350  vonvolmbl  41351  sssmf  41423  incsmf  41427  issmflelem  41429  issmfle  41430  smfconst  41434  issmfgtlem  41440  issmfgt  41441  smfaddlem2  41448  decsmf  41451  issmfgelem  41453  issmfge  41454  nsssmfmbflem  41462  smfpimioo  41470  smfresal  41471  smfmullem4  41477  smfpimbor1lem1  41481  smf2id  41484  upwlksfval  42278
  Copyright terms: Public domain W3C validator