Theorem ssexd 5285

Description: A subclass of a set is a set. Deduction form of ssexg 5280. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
ssexd.1	⊢ (𝜑 → 𝐵 ∈ 𝐶)
ssexd.2	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
ssexd	⊢ (𝜑 → 𝐴 ∈ V)

Proof of Theorem ssexd

Step	Hyp	Ref	Expression
1		ssexd.2	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssexd.1	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
3		ssexg 5280	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  abexd  5286  sselpwd  5289  sepab  5293  moabex  5425  opabbrex  7473  soex  7933  fex2  7948  fabexd  7949  mapex  7952  funexw  7964  opabex2  8068  fnwelem  8143  fnse  8150  extmptsuppeq  8205  f1setex  8879  f1imaen2g  9042  fsuppss  9375  ordtypelem10  9521  oismo  9534  wofib  9539  wdom2d  9574  wdomd  9575  unxpwdom2  9582  ttrclexg  9724  djuexALT  10003  acni2  10125  fin1a2lem12  10489  hsmexlem1  10504  zorn2lem4  10577  ondomon  10647  fpwwe2lem2  10717  fpwwe2lem4  10719  fpwwe2lem11  10726  fpwwe2  10728  fpwwelem  10730  canthwelem  10735  pwfseqlem4  10747  hashpss  14554  hashf1lem1  14600  trclfv  15153  hashbcss  17182  strssd  17383  restid2  17601  divsfval  17719  mrieqv2d  17813  mrissmrcd  17814  mreexexlemd  17818  mreexexlem3d  17820  mreexexlem4d  17821  mreexdomd  17823  rescabs  18008  rescabs2  18009  resssetc  18267  resscatc  18284  estrres  18313  yonedalem1  18446  yonedalem21  18447  yonedalem3a  18448  yonedalem4c  18451  yonedalem22  18452  yonedalem3b  18453  yonedainv  18455  yonffthlem  18456  joinfval  18545  meetfval  18559  acsdomd  18731  idressid  18862  ressmulgnnd  19288  gass  19515  pmtrfconj  19680  sylow2blem2  19835  dprdres  20244  dmdprdsplitlem  20253  primefld  21062  pwssplit0  21333  pwssplit1  21334  pwssplit2  21335  pwssplit3  21336  frlmsplit2  22079  frlmsslss  22080  psrbagres  22238  opsrtoslem2  22365  evlsgsumadd  22405  evlsgsummul  22406  selvcllemh  22446  selvcllem4  22447  selvcllem5  22448  selvcl  22449  selvval2  22450  selvvvval  22451  selvadd  22452  selvmul  22453  evls1gsumadd  22642  evls1gsummul  22643  evl1gsummul  22678  neiptoptop  23449  lpval  23457  neitr  23498  ordtbaslem  23506  ordtrest2  23522  cnrest2  23604  cnpresti  23606  cnprest  23607  cnprest2  23608  connsuba  23738  connsubclo  23742  unconn  23747  1stcelcls  23780  hausmapdom  23819  dissnref  23847  ptbasfi  23900  ptcls  23935  cnmpt2res  23996  qtopval2  24015  elqtop  24016  qtoprest  24036  ptuncnv  24126  ptunhmeo  24127  fsubbas  24186  elfm  24266  rnelfmlem  24271  rnelfm  24272  fmfnfmlem4  24276  flimclslem  24303  hauspwpwdom  24307  ptcmplem1  24371  cnextcn  24386  cnextfres1  24387  isust  24523  trust  24548  elutop  24552  restutop  24556  trcfilu  24612  cfiluweak  24613  psmetres2  24633  xmetres2  24680  fmcfil  25593  dvaddf  26262  dvmulf  26263  dvcmulf  26265  dvcof  26268  ulmss  26724  nosupno  28060  noinfno  28075  ssslts1  28159  ssslts2  28160  ltonsex  28648  perpln1  29185  perpln2  29186  isperp  29187  wksfval  30190  fnpreimac  33264  fisuppov1  33276  resf1o  33322  gsumpart  33624  gsumwrd2dccat  33639  cycpmco2lem5  33691  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem3  33805  elrgspnlem4  33806  elrgspn  33807  erlval  33819  rlocval  33820  rlocbas  33829  fldgenval  33874  islinds5  33923  ellspds  33924  elrsp  33927  elrspunidl  33978  mplasclco  34148  selvascl  34149  evlextv  34174  psrmonprod  34184  esplympl  34199  resssra  34219  lbslelsp  34230  lbsdiflsp0  34258  irngval  34317  ordtrest2NEW  34555  lmlim  34579  esummono  34686  esumrnmpt2  34700  esumpinfval  34705  elcarsg  34937  carsgmon  34946  carsggect  34950  reprval  35239  repr0  35240  reprsuc  35244  reprss  35246  reprinrn  35247  reprlt  35248  reprgt  35250  reprinfz1  35251  reprpmtf1o  35255  reprdifc  35256  bnj1413  35665  cvmliftmolem1  36046  satf0suclem  36140  fwddifval  36927  neibastop1  37147  neibastop2lem  37148  fnejoin1  37156  filnetlem3  37168  filnetlem4  37169  weiunse  37256  numiunnum  37258  bj-imdirval2lem  38104  bj-imdirval3  38106  bj-imdirco  38112  dissneqlem  38264  aks6d1c2lem4  43178  sticksstones20  43217  aks6d1c6lem3  43223  evlselv  43618  fsuppssindlem2  43621  fsuppssind  43622  elrfi  43705  elrfirn2  43707  oaun3lem3  44378  nadd2rabex  44388  clcnvlem  44623  relexpss1d  44705  k0004lem2  45148  ixpssmapc  46090  restuni4  46136  restsubel  46168  wessf1ornlem  46200  unirnmap  46221  inmap  46222  difmapsn  46225  unirnmapsn  46227  ssmapsn  46229  limsupre  46651  limsuppnfdlem  46711  limsuppnflem  46720  limsupmnflem  46730  limsupre2lem  46734  liminfval4  46799  liminfval3  46800  icccncfext  46897  dvdivcncf  46937  dvnprodlem1  46956  dvnprodlem2  46957  ovolsplit  46998  stoweidlem31  47041  stoweidlem53  47063  stoweidlem57  47067  stoweidlem59  47069  etransclem46  47290  salexct  47344  subsaluni  47370  fsumlesge0  47387  sge0iunmptlemfi  47423  sge0iunmptlemre  47425  meadjuni  47467  meadjiunlem  47475  omessle  47508  omecl  47513  isomenndlem  47540  caragencmpl  47545  ovnval2  47555  ovnval2b  47562  ovncvrrp  47574  ovncl  47577  hoidmvlelem2  47606  hoidmvlelem3  47607  ovncvr2  47621  ovnsubadd2lem  47655  ovnovollem3  47668  vonvolmbllem  47670  vonvolmbl  47671  sssmf  47748  incsmf  47752  issmflelem  47754  issmfle  47755  smfconst  47759  issmfgtlem  47765  issmfgt  47766  smfaddlem2  47774  decsmf  47777  issmfgelem  47779  issmfge  47780  nsssmfmbflem  47788  smfpimioo  47797  smfresal  47798  smfmullem4  47804  smfpimbor1lem1  47808  smf2id  47811  tmachlem-agreeself  47946  tmachlem-agreeprod  47947  tmachlem-uassst  47953  tmachlem-extpcover  47955  tmachlem-agreefin  47958  upwlksfval  49233  toplatglb  50109