Theorem ssel 3868

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

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1540   = wceq 1542  ∃wex 1786   ∈ wcel 2113   ⊆ wss 3841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858

This theorem is referenced by:  ssel2  3870  sseli  3871  sseld  3874  sstr2  3882  nelss  3938  ssrexf  3939  ssralv  3941  ssrexv  3942  ralss  3945  rexss  3946  ssconb  4026  sscon  4027  ssdif  4028  unss1  4067  ssrin  4122  difin2  4180  reuss2  4201  reupick  4205  elpwunsn  4571  sssn  4711  uniss  4801  ss2iun  4896  ssiun  4929  iinss  4939  disjss2  4995  disjss1  4998  pwnss  5213  sspwb  5305  ssopab2bw  5399  ssopab2b  5401  pwssun  5421  xpss12  5534  frinxp  5599  ssrel  5622  ssrel2  5624  ssrelrel  5634  dmss  5739  elreldm  5772  dmcosseq  5810  relssres  5860  iss  5871  resopab2  5872  ssrnres  6004  dfco2a  6073  cores  6076  oneqmini  6217  sucssel  6258  onssneli  6276  onssnel2i  6277  funssres  6377  fununi  6408  dfimafn  6726  funimass4  6728  funimass3  6825  dff3  6870  dff4  6871  funfvima2  6998  funfvima3  7003  f1elima  7026  isomin  7097  isofrlem  7100  riotass2  7152  ssoprab2b  7231  eqoprab2bw  7232  resoprab2  7279  ssorduni  7513  onint  7523  oninton  7528  ssnlim  7612  releldm2  7760  dmtpos  7926  wfrlem10  7986  onfununi  8000  tz7.48lem  8099  tz7.49  8103  omeulem1  8232  omeulem2  8233  omsmolem  8304  omsmo  8305  ss2ixp  8513  boxriin  8543  onomeneq  8781  unblem1  8837  unblem3  8839  fiint  8862  inf3lem2  9158  cantnflem2  9219  tcel  9253  tz9.13  9286  rankr1ag  9297  rankpwi  9318  rankelb  9319  bndrank  9336  cardlim  9467  carduni  9476  acni2  9539  dfac12r  9639  cfub  9742  cflim2  9756  fin1a2lem9  9901  axdc3lem2  9944  axdclem2  10013  gch2  10168  eltsk2g  10244  suplem1pr  10545  negn0  11140  negf1o  11141  negfi  11660  lbreu  11661  lbinf  11664  sup2  11667  sup3  11668  infm3  11670  infregelb  11695  uzwo  12386  eqreznegel  12409  xrsupsslem  12776  xrinfmsslem  12777  supxrpnf  12787  supxrunb1  12788  supxrunb2  12789  iccsupr  12909  ssnn0fi  13437  incexclem  15277  fprodmodd  15436  sumeven  15825  sumodd  15826  gcdcllem1  15935  lcmfnnval  16058  lcmfnncl  16063  dvdslcmf  16065  lcmfunsnlem2lem2  16073  lcmfdvdsb  16077  lubel  17841  clatleglb  17845  smndex1mgm  18181  smndex1sgrp  18182  smndex1mnd  18184  mulgpropd  18380  sylow2a  18855  efgi2  18962  lspsnel6  19878  submabas  21322  pmatcollpw3lem  21527  elcls2  21818  isclo2  21832  cmpsublem  22143  cmpsub  22144  hauscmplem  22150  1stcelcls  22205  llyss  22223  nllyss  22224  txkgen  22396  nrmr0reg  22493  uffix  22665  ufinffr  22673  ufilen  22674  fmfnfmlem2  22699  alexsubALTlem2  22792  alexsubALT  22795  metrest  23270  iccntr  23566  reconnlem2  23572  clmneg1  23827  clmvscom  23835  caubl  24053  ulmss  25136  axcontlem4  26905  ocsh  29210  ococss  29220  shorth  29222  spansnss2  29502  h1datomi  29508  pjss2i  29607  pjssmii  29608  pjorthcoi  30096  pj3si  30134  ssrelf  30521  dfimafnf  30537  funimass4f  30538  mptssALT  30579  1stpreima  30606  2ndpreima  30607  isprmidlc  31187  ordtconnlem1  31438  indpi1  31550  bnj518  32429  nummin  32626  cvmlift2lem1  32827  satffunlem2lem1  32929  satfvel  32937  dfon2lem6  33328  trpredmintr  33365  orderseqlem  33404  nofv  33493  nocvxminlem  33605  nocvxmin  33606  limsucncmpi  34264  finxpreclem4  35177  poimirlem3  35392  poimirlem29  35418  poimirlem32  35421  ismtyres  35578  ispridlc  35840  iss2  36091  paddss1  37443  paddss2  37444  lspindp5  39396  sn-sup2  40000  dffltz  40027  pw2f1ocnv  40415  ss2iundf  40797  iunrelexp0  40840  gneispace0nelrn3  41282  nzss  41457  onfrALTlem3  41686  onfrALTlem2  41688  sspwtr  41963  sspwtrALT  41964  sspwtrALT2  41965  pwtrVD  41966  pwtrrVD  41967  suctrALT2VD  41978  suctrALT2  41979  onfrALTlem3VD  42029  onfrALTlem2VD  42031  iinssf  42209  qndenserrnopnlem  43364  dfaimafn  44174  sprsymrelfolem2  44463  mgmplusfreseq  44845  gsumlsscl  45237  lincfsuppcl  45272  linccl  45273  onsetrec  45850