Theorem ssexd 5274

Description: A subclass of a set is a set. Deduction form of ssexg 5273. (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 5273	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  abexd  5275  sselpwd  5278  opabbrex  7423  soex  7878  fex2  7893  fabexd  7894  mapex  7898  funexw  7911  opabex2  8016  fnwelem  8088  fnse  8090  extmptsuppeq  8145  f1setex  8808  f1imaen2g  8964  fsuppss  9311  ordtypelem10  9457  oismo  9470  wofib  9475  wdom2d  9510  wdomd  9511  unxpwdom2  9518  ttrclexg  9655  djuexALT  9854  acni2  9978  fin1a2lem12  10343  hsmexlem1  10358  zorn2lem4  10431  fpwwe2lem2  10564  fpwwe2lem4  10566  fpwwe2lem11  10573  fpwwe2  10575  fpwwelem  10577  canthwelem  10582  pwfseqlem4  10594  hashf1lem1  14399  trclfv  14944  hashbcss  16953  strssd  17153  restid2  17371  divsfval  17488  mrieqv2d  17582  mrissmrcd  17583  mreexexlemd  17587  mreexexlem3d  17589  mreexexlem4d  17590  mreexdomd  17592  rescabs  17777  rescabs2  17778  resssetc  18036  resscatc  18053  estrres  18082  yonedalem1  18215  yonedalem21  18216  yonedalem3a  18217  yonedalem4c  18220  yonedalem22  18221  yonedalem3b  18222  yonedainv  18224  yonffthlem  18225  joinfval  18314  meetfval  18328  acsdomd  18500  ressmulgnnd  18994  gass  19217  pmtrfconj  19382  sylow2blem2  19537  dprdres  19946  dmdprdsplitlem  19955  primefld  20727  pwssplit0  20999  pwssplit1  21000  pwssplit2  21001  pwssplit3  21002  frlmsplit2  21717  frlmsslss  21718  opsrtoslem2  21998  evlsgsumadd  22033  evlsgsummul  22034  evls1gsumadd  22246  evls1gsummul  22247  evl1gsummul  22282  neiptoptop  23053  lpval  23061  neitr  23102  ordtbaslem  23110  ordtrest2  23126  cnrest2  23208  cnpresti  23210  cnprest  23211  cnprest2  23212  connsuba  23342  connsubclo  23346  unconn  23351  1stcelcls  23383  hausmapdom  23422  dissnref  23450  ptbasfi  23503  ptcls  23538  cnmpt2res  23599  qtopval2  23618  elqtop  23619  qtoprest  23639  ptuncnv  23729  ptunhmeo  23730  fsubbas  23789  elfm  23869  rnelfmlem  23874  rnelfm  23875  fmfnfmlem4  23879  flimclslem  23906  hauspwpwdom  23910  ptcmplem1  23974  cnextcn  23989  cnextfres1  23990  isust  24126  trust  24152  elutop  24156  restutop  24160  trcfilu  24216  cfiluweak  24217  psmetres2  24237  xmetres2  24284  fmcfil  25207  dvaddf  25880  dvmulf  25881  dvcmulf  25883  dvcof  25887  ulmss  26341  nosupno  27650  noinfno  27665  sssslt1  27743  sssslt2  27744  sltonex  28205  perpln1  28692  perpln2  28693  isperp  28694  wksfval  29592  fnpreimac  32647  fisuppov1  32658  resf1o  32705  hashpss  32786  gsumpart  33042  gsumwrd2dccat  33052  cycpmco2lem5  33104  elrgspnlem1  33211  elrgspnlem2  33212  elrgspnlem3  33213  elrgspnlem4  33214  elrgspn  33215  erlval  33227  rlocval  33228  rlocbas  33236  fldgenval  33280  islinds5  33333  ellspds  33334  elrsp  33338  elrspunidl  33394  resssra  33578  lbslelsp  33588  lbsdiflsp0  33617  irngval  33675  ordtrest2NEW  33908  lmlim  33932  esummono  34039  esumrnmpt2  34053  esumpinfval  34058  elcarsg  34291  carsgmon  34300  carsggect  34304  reprval  34596  repr0  34597  reprsuc  34601  reprss  34603  reprinrn  34604  reprlt  34605  reprgt  34607  reprinfz1  34608  reprpmtf1o  34612  reprdifc  34613  bnj1413  35020  cvmliftmolem1  35263  satf0suclem  35357  fwddifval  36145  neibastop1  36342  neibastop2lem  36343  fnejoin1  36351  filnetlem3  36363  filnetlem4  36364  weiunse  36451  numiunnum  36453  bj-imdirval2lem  37165  bj-imdirval3  37167  bj-imdirco  37173  dissneqlem  37323  aks6d1c2lem4  42110  sticksstones20  42149  aks6d1c6lem3  42155  psrbagres  42529  selvcllemh  42563  selvcllem4  42564  selvcllem5  42565  selvcl  42566  selvval2  42567  selvvvval  42568  evlselv  42570  selvadd  42571  selvmul  42572  fsuppssindlem2  42575  fsuppssind  42576  elrfi  42677  elrfirn2  42679  oaun3lem3  43360  nadd2rabex  43370  clcnvlem  43607  relexpss1d  43689  k0004lem2  44132  ixpssmapc  45062  restuni4  45110  restsubel  45142  wessf1ornlem  45174  disjinfi  45181  unirnmap  45197  inmap  45198  difmapsn  45201  unirnmapsn  45203  ssmapsn  45205  limsupre  45634  limsuppnfdlem  45694  limsuppnflem  45703  limsupmnflem  45713  limsupre2lem  45717  liminfval4  45782  liminfval3  45783  icccncfext  45880  dvdivcncf  45920  dvnprodlem1  45939  dvnprodlem2  45940  ovolsplit  45981  stoweidlem31  46024  stoweidlem53  46046  stoweidlem57  46050  stoweidlem59  46052  etransclem46  46273  salexct  46327  subsaluni  46353  fsumlesge0  46370  sge0iunmptlemfi  46406  sge0iunmptlemre  46408  meadjuni  46450  meadjiunlem  46458  omessle  46491  omecl  46496  isomenndlem  46523  caragencmpl  46528  ovnval2  46538  ovnval2b  46545  ovncvrrp  46557  ovncl  46560  hoidmvlelem2  46589  hoidmvlelem3  46590  ovncvr2  46604  ovnsubadd2lem  46638  ovnovollem3  46651  vonvolmbllem  46653  vonvolmbl  46654  sssmf  46731  incsmf  46735  issmflelem  46737  issmfle  46738  smfconst  46742  issmfgtlem  46748  issmfgt  46749  smfaddlem2  46757  decsmf  46760  issmfgelem  46762  issmfge  46763  nsssmfmbflem  46771  smfpimioo  46780  smfresal  46781  smfmullem4  46787  smfpimbor1lem1  46791  smf2id  46794  upwlksfval  48118  toplatglb  48984