Theorem ssel 3932

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2216. (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 3923	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 23	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 624	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1865	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2841	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2841	. . 3 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
7	4, 5, 6	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
8	1, 7	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2840  df-ss 3923

This theorem is used by:  ssel2  3933  sseli  3934  sseld  3937  nelss  4004  ssrexf  4005  ralssOLD  4013  rexssOLD  4014  rabss2  4032  ssconb  4096  sscon  4097  ssdif  4098  unss1  4138  ssrin  4194  difin2  4254  reuss2  4279  reupick  4282  elpwunsn  4652  sssn  4794  uniss  4882  ss2iun  4977  ssiun  5013  iinss  5023  disjss2  5081  disjss1  5084  pwnss  5324  sspwb  5432  ssopab2bw  5534  ssopab2b  5536  pwssun  5555  xpss12  5678  frinxp  5746  ssrel  5771  ssrel2  5773  ssrelrel  5784  dmss  5894  elreldm  5927  dmcosseq  5970  dmcosseqOLD  5971  relssres  6023  iss  6039  resopab2  6040  ssrnres  6178  imadifssran  6204  imadifssranOLD  6205  dfco2a  6249  cores  6252  oneqmini  6418  sucssel  6462  onssneli  6482  onssnel2i  6483  funssres  6584  fununi  6615  dfimafn  6947  funimass4  6949  funimass3  7053  dff3  7099  dff4  7100  funfvima2  7236  funfvima3  7241  f1elima  7266  isomin  7344  isofrlem  7347  riotass2  7406  ssoprab2b  7488  eqoprab2bw  7489  resoprab2  7538  ssorduni  7784  onint  7795  oninton  7800  ssnlim  7888  mptcnfimad  7989  releldm2  8046  orderseqlem  8159  dmtpos  8240  onfununi  8334  tz7.48lem  8434  tz7.49  8438  omeulem1  8573  omeulem2  8574  omsmolem  8649  omsmo  8650  ss2ixp  8914  boxriin  8944  unblem1  9259  unblem3  9261  fiint  9293  inf3lem2  9605  cantnflem2  9666  tcel  9719  tz9.13  9770  rankr1ag  9781  rankpwi  9802  rankelb  9803  bndrank  9820  cardlim  9974  carduni  9983  acni2  10046  dfac12r  10146  cfub  10247  cflim2  10262  fin1a2lem9  10407  axdc3lem2  10450  axdclem2  10519  gch2  10675  eltsk2g  10751  suplem1pr  11052  negn0  11658  negf1o  11659  negfi  12179  lbreu  12180  lbinf  12183  sup2  12186  sup3  12187  infm3  12189  infregelb  12214  indpi1  12247  uzwo  12951  eqreznegel  12974  xrsupsslem  13349  xrinfmsslem  13350  supxrpnf  13360  supxrunb1  13361  supxrunb2  13362  iccsupr  13485  ssnn0fi  14039  incexclem  15913  fprodmodd  16074  sumeven  16467  sumodd  16468  gcdcllem1  16579  lcmfnnval  16704  lcmfnncl  16709  dvdslcmf  16711  lcmfunsnlem2lem2  16719  lcmfdvdsb  16723  lubel  18592  clatleglb  18596  smndex1mgm  19006  smndex1sgrp  19007  smndex1mnd  19009  mulgpropd  19226  sylow2a  19733  efgi2  19839  ellspsn6  21165  rnglidlmcl  21391  lidlunin0  21411  unichnlidl  21412  isprmidlc  21522  submabas  22785  pmatcollpw3lem  22990  elcls2  23281  isclo2  23295  cmpsublem  23606  cmpsub  23607  hauscmplem  23613  1stcelcls  23669  llyss  23687  nllyss  23688  txkgen  23860  nrmr0reg  23957  uffix  24129  ufinffr  24137  ufilen  24138  fmfnfmlem2  24163  alexsubALTlem2  24256  alexsubALT  24259  metrest  24732  iccntr  25030  reconnlem2  25036  clmneg1  25292  clmvscom  25300  caubl  25518  dvply2g  26497  ulmss  26611  nofv  27872  nocvxminlem  27998  nocvxmin  27999  axcontlem4  29372  ocsh  31706  ococss  31716  shorth  31718  spansnss2  31998  h1datomi  32004  pjss2i  32103  pjssmii  32104  pjorthcoi  32592  pj3si  32630  ssrelf  33031  dfimafnf  33052  funimass4f  33053  mptssALT  33090  1stpreima  33123  2ndpreima  33124  ordtconnlem1  34378  bnj518  35339  fissorduni  35538  nummin  35542  tz9.1regs  35604  cvmlift2lem1  35831  satffunlem2lem1  35933  satfvel  35941  dfon2lem6  36315  limsucncmpi  37013  finxpreclem4  38097  poimirlem3  38331  poimirlem29  38357  poimirlem32  38360  ismtyres  38517  ispridlc  38779  iss2  39051  paddss1  40649  paddss2  40650  lspindp5  42602  sn-sup2  43323  sn-sup3d  43324  dffltz  43424  pw2f1ocnv  43822  onsupmaxb  44024  naddwordnexlem2  44183  ss2iundf  44443  iunrelexp0  44486  gneispace0nelrn3  44926  nzss  45085  onfrALTlem3  45311  onfrALTlem2  45313  sspwtr  45587  sspwtrALT  45588  sspwtrALT2  45589  pwtrVD  45590  pwtrrVD  45591  suctrALT2VD  45602  suctrALT2  45603  onfrALTlem3VD  45653  onfrALTlem2VD  45655  relpmin  45719  relpfrlem  45720  ssclaxsep  45749  omssaxinf2  45755  iinssf  45914  qndenserrnopnlem  47069  dfaimafn  47960  sprsymrelfolem2  48300  mgmplusfreseq  48987  gsumlsscl  49217  lincfsuppcl  49250  linccl  49251  onsetrec  50543