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  5301  sspwb  5406  ssopab2bw  5505  ssopab2b  5507  pwssun  5526  xpss12  5649  frinxp  5717  ssrel  5742  ssrel2  5744  ssrelrel  5755  dmss  5861  elreldm  5894  dmcosseq  5937  dmcosseqOLD  5938  dmcosseqOLDOLD  5939  relssres  5991  iss  6004  resopab2  6005  imadifssran  6119  ssrnres  6146  dfco2a  6214  cores  6217  oneqmini  6380  sucssel  6424  onssneli  6444  onssnel2i  6445  funssres  6546  fununi  6577  dfimafn  6906  funimass4  6908  funimass3  7010  dff3  7056  dff4  7057  funfvima2  7189  funfvima3  7194  f1elima  7221  isomin  7295  isofrlem  7298  riotass2  7357  ssoprab2b  7439  eqoprab2bw  7440  resoprab2  7489  ssorduni  7736  onint  7747  oninton  7752  ssnlim  7840  mptcnfimad  7942  releldm2  7999  orderseqlem  8111  dmtpos  8192  onfununi  8285  tz7.48lem  8384  tz7.49  8388  omeulem1  8521  omeulem2  8522  omsmolem  8597  omsmo  8598  ss2ixp  8862  boxriin  8892  unblem1  9206  unblem3  9208  fiint  9241  inf3lem2  9552  cantnflem2  9613  tcel  9666  tz9.13  9717  rankr1ag  9728  rankpwi  9749  rankelb  9750  bndrank  9767  cardlim  9898  carduni  9907  acni2  9970  dfac12r  10071  cfub  10173  cflim2  10187  fin1a2lem9  10332  axdc3lem2  10375  axdclem2  10444  gch2  10600  eltsk2g  10676  suplem1pr  10977  negn0  11580  negf1o  11581  negfi  12105  lbreu  12106  lbinf  12109  sup2  12112  sup3  12113  infm3  12115  infregelb  12140  uzwo  12838  eqreznegel  12861  xrsupsslem  13236  xrinfmsslem  13237  supxrpnf  13247  supxrunb1  13248  supxrunb2  13249  iccsupr  13372  ssnn0fi  13922  incexclem  15773  fprodmodd  15934  sumeven  16328  sumodd  16329  gcdcllem1  16440  lcmfnnval  16565  lcmfnncl  16570  dvdslcmf  16572  lcmfunsnlem2lem2  16580  lcmfdvdsb  16584  lubel  18451  clatleglb  18455  smndex1mgm  18849  smndex1sgrp  18850  smndex1mnd  18852  mulgpropd  19063  sylow2a  19565  efgi2  19671  ellspsn6  20962  rnglidlmcl  21188  submabas  22539  pmatcollpw3lem  22744  elcls2  23035  isclo2  23049  cmpsublem  23360  cmpsub  23361  hauscmplem  23367  1stcelcls  23422  llyss  23440  nllyss  23441  txkgen  23613  nrmr0reg  23710  uffix  23882  ufinffr  23890  ufilen  23891  fmfnfmlem2  23916  alexsubALTlem2  24009  alexsubALT  24012  metrest  24485  iccntr  24783  reconnlem2  24789  clmneg1  25055  clmvscom  25063  caubl  25281  dvply2g  26265  ulmss  26379  nofv  27642  nocvxminlem  27767  nocvxmin  27768  axcontlem4  29058  ocsh  31377  ococss  31387  shorth  31389  spansnss2  31669  h1datomi  31675  pjss2i  31774  pjssmii  31775  pjorthcoi  32263  pj3si  32301  ssrelf  32711  dfimafnf  32732  funimass4f  32733  mptssALT  32770  1stpreima  32803  2ndpreima  32804  indpi1  32958  isprmidlc  33546  ordtconnlem1  34108  bnj518  35068  fissorduni  35273  nummin  35276  tz9.1regs  35318  cvmlift2lem1  35524  satffunlem2lem1  35626  satfvel  35634  dfon2lem6  36008  limsucncmpi  36667  finxpreclem4  37676  poimirlem3  37903  poimirlem29  37929  poimirlem32  37932  ismtyres  38088  ispridlc  38350  iss2  38624  paddss1  40222  paddss2  40223  lspindp5  42175  sn-sup2  42890  sn-sup3d  42891  dffltz  43021  pw2f1ocnv  43423  onsupmaxb  43625  naddwordnexlem2  43784  ss2iundf  44044  iunrelexp0  44087  gneispace0nelrn3  44527  nzss  44702  onfrALTlem3  44929  onfrALTlem2  44931  sspwtr  45205  sspwtrALT  45206  sspwtrALT2  45207  pwtrVD  45208  pwtrrVD  45209  suctrALT2VD  45220  suctrALT2  45221  onfrALTlem3VD  45271  onfrALTlem2VD  45273  relpmin  45337  relpfrlem  45338  ssclaxsep  45367  omssaxinf2  45373  iinssf  45526  qndenserrnopnlem  46684  dfaimafn  47554  sprsymrelfolem2  47882  mgmplusfreseq  48554  gsumlsscl  48769  lincfsuppcl  48802  linccl  48803  onsetrec  50096