Theorem ssel 3929

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2185. (Revised by SN, 27-May-2024.)

Assertion

Ref	Expression
ssel	⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem ssel

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ss 3920	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 22	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 613	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1834	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2813	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2813	. . 3 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
7	4, 5, 6	3imtr4g 296	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
8	1, 7	sylbi 217	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3920

This theorem is referenced by:  ssel2  3930  sseli  3931  sseld  3934  sstr2OLD  3943  nelss  4001  ssrexf  4002  ssralvOLD  4008  ssrexvOLD  4009  ralssOLD  4012  rexssOLD  4013  rabss2  4031  ssconb  4096  sscon  4097  ssdif  4098  unss1  4139  ssrin  4196  difin2  4255  reuss2  4280  reupick  4283  elpwunsn  4643  sssn  4784  uniss  4873  ss2iun  4967  ssiun  5004  iinss  5014  disjss2  5070  disjss1  5073  pwnss  5299  sspwb  5404  ssopab2bw  5503  ssopab2b  5505  pwssun  5524  xpss12  5647  frinxp  5715  ssrel  5740  ssrel2  5742  ssrelrel  5753  dmss  5859  elreldm  5892  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  relssres  5989  iss  6002  resopab2  6003  imadifssran  6117  ssrnres  6144  dfco2a  6212  cores  6215  oneqmini  6378  sucssel  6422  onssneli  6442  onssnel2i  6443  funssres  6544  fununi  6575  dfimafn  6904  funimass4  6906  funimass3  7008  dff3  7054  dff4  7055  funfvima2  7187  funfvima3  7192  f1elima  7219  isomin  7293  isofrlem  7296  riotass2  7355  ssoprab2b  7437  eqoprab2bw  7438  resoprab2  7487  ssorduni  7734  onint  7745  oninton  7750  ssnlim  7838  mptcnfimad  7940  releldm2  7997  orderseqlem  8109  dmtpos  8190  onfununi  8283  tz7.48lem  8382  tz7.49  8386  omeulem1  8519  omeulem2  8520  omsmolem  8595  omsmo  8596  ss2ixp  8860  boxriin  8890  unblem1  9204  unblem3  9206  fiint  9239  inf3lem2  9550  cantnflem2  9611  tcel  9664  tz9.13  9715  rankr1ag  9726  rankpwi  9747  rankelb  9748  bndrank  9765  cardlim  9896  carduni  9905  acni2  9968  dfac12r  10069  cfub  10171  cflim2  10185  fin1a2lem9  10330  axdc3lem2  10373  axdclem2  10442  gch2  10598  eltsk2g  10674  suplem1pr  10975  negn0  11578  negf1o  11579  negfi  12103  lbreu  12104  lbinf  12107  sup2  12110  sup3  12111  infm3  12113  infregelb  12138  uzwo  12836  eqreznegel  12859  xrsupsslem  13234  xrinfmsslem  13235  supxrpnf  13245  supxrunb1  13246  supxrunb2  13247  iccsupr  13370  ssnn0fi  13920  incexclem  15771  fprodmodd  15932  sumeven  16326  sumodd  16327  gcdcllem1  16438  lcmfnnval  16563  lcmfnncl  16568  dvdslcmf  16570  lcmfunsnlem2lem2  16578  lcmfdvdsb  16582  lubel  18449  clatleglb  18453  smndex1mgm  18844  smndex1sgrp  18845  smndex1mnd  18847  mulgpropd  19058  sylow2a  19560  efgi2  19666  ellspsn6  20957  rnglidlmcl  21183  submabas  22534  pmatcollpw3lem  22739  elcls2  23030  isclo2  23044  cmpsublem  23355  cmpsub  23356  hauscmplem  23362  1stcelcls  23417  llyss  23435  nllyss  23436  txkgen  23608  nrmr0reg  23705  uffix  23877  ufinffr  23885  ufilen  23886  fmfnfmlem2  23911  alexsubALTlem2  24004  alexsubALT  24007  metrest  24480  iccntr  24778  reconnlem2  24784  clmneg1  25050  clmvscom  25058  caubl  25276  dvply2g  26260  ulmss  26374  nofv  27637  nocvxminlem  27762  nocvxmin  27763  axcontlem4  29052  ocsh  31371  ococss  31381  shorth  31383  spansnss2  31663  h1datomi  31669  pjss2i  31768  pjssmii  31769  pjorthcoi  32257  pj3si  32295  ssrelf  32705  dfimafnf  32726  funimass4f  32727  mptssALT  32764  1stpreima  32797  2ndpreima  32798  indpi1  32952  isprmidlc  33540  ordtconnlem1  34102  bnj518  35062  fissorduni  35267  nummin  35270  tz9.1regs  35312  cvmlift2lem1  35518  satffunlem2lem1  35620  satfvel  35628  dfon2lem6  36002  limsucncmpi  36661  finxpreclem4  37649  poimirlem3  37874  poimirlem29  37900  poimirlem32  37903  ismtyres  38059  ispridlc  38321  iss2  38595  paddss1  40193  paddss2  40194  lspindp5  42146  sn-sup2  42861  sn-sup3d  42862  dffltz  42992  pw2f1ocnv  43394  onsupmaxb  43596  naddwordnexlem2  43755  ss2iundf  44015  iunrelexp0  44058  gneispace0nelrn3  44498  nzss  44673  onfrALTlem3  44900  onfrALTlem2  44902  sspwtr  45176  sspwtrALT  45177  sspwtrALT2  45178  pwtrVD  45179  pwtrrVD  45180  suctrALT2VD  45191  suctrALT2  45192  onfrALTlem3VD  45242  onfrALTlem2VD  45244  relpmin  45308  relpfrlem  45309  ssclaxsep  45338  omssaxinf2  45344  iinssf  45497  qndenserrnopnlem  46655  dfaimafn  47525  sprsymrelfolem2  47853  mgmplusfreseq  48525  gsumlsscl  48740  lincfsuppcl  48773  linccl  48774  onsetrec  50067