Theorem ssel 3907

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 3901	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 23	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 624	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1865	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2840	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2840	. . 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 2147   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

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

This theorem is used by:  ssel2  3908  sseli  3909  sseld  3912  nelss  3979  ssrexf  3980  rabss2  4005  ssconb  4081  sscon  4082  ssdif  4083  ssrin  4141  unss1  4186  difin2  4249  reuss2  4274  reupick  4277  elpwunsn  4646  sssn  4787  uniss  4880  ss2iun  4975  ssiun  5010  iinss  5020  disjss2  5078  disjss1  5081  pwnss  5320  sspwb  5424  ssopab2bw  5529  ssopab2b  5531  pwssun  5550  xpss12  5673  frinxp  5742  ssrel  5767  ssrelOLD  5768  ssrel2  5770  ssrelrel  5781  dmss  5896  elreldm  5929  dmcosseq  5972  dmcosseqOLD  5973  relssres  6029  iss  6045  resopab2  6046  dfrn7  6084  ssrnres  6188  imadifssranOLD  6221  imadifssranOLDOLD  6222  dfco2a  6266  cores  6269  oneqmini  6442  sucssel  6486  onssneli  6506  onssnel2i  6507  funssres  6612  fununi  6645  dfimafn  6978  funimass4  6980  funimass3  7084  dff3  7132  dff4  7133  funfvima2  7268  funfvima3  7273  f1elima  7298  isomin  7376  isofrlem  7379  riotass2  7438  ssoprab2b  7520  eqoprab2bw  7521  resoprab2  7570  ssorduni  7827  onint  7838  oninton  7843  ssnlim  7931  mptcnfimad  8032  releldm2  8088  orderseqlem  8211  dmtpos  8293  onfununi  8387  tz7.48lemOLD  8489  tz7.49  8493  omeulem1  8628  omeulem2  8629  omsmolem  8704  omsmo  8705  ss2ixp  8976  boxriin  9006  fissorduni  9320  unblem1  9322  unblem3  9324  fiint  9356  inf3lem2  9667  cantnflem2  9728  tcel  9781  tz9.13  9835  rankr1ag  9847  rankpwi  9869  rankelb  9870  bndrank  9891  cardlim  10090  carduni  10101  acni2  10164  dfac12r  10264  cfub  10365  cflim2  10380  fin1a2lem9  10525  axdc3lem2  10568  axdclem2  10637  gch2  10799  eltsk2g  10875  suplem1pr  11176  negn0  11784  negf1o  11785  negfi  12306  lbreu  12307  lbinf  12310  sup2  12313  sup3  12314  infm3  12316  infregelb  12341  indpi1  12374  uzwo  13078  eqreznegel  13101  xrsupsslem  13477  xrinfmsslem  13478  supxrpnf  13488  supxrunb1  13489  supxrunb2  13490  iccsupr  13613  ssnn0fi  14168  incexclem  16049  fprodmodd  16208  sumeven  16601  sumodd  16602  gcdcllem1  16713  lcmfnnval  16843  lcmfnncl  16848  dvdslcmf  16850  lcmfunsnlem2lem2  16858  lcmfdvdsb  16862  lubel  18738  clatleglb  18742  smndex1mgm  19156  smndex1sgrp  19157  smndex1mnd  19159  mulgpropd  19376  sylow2a  19884  efgi2  19990  ellspsn6  21320  rnglidlmcl  21546  lidlunin0  21566  unichnlidl  21567  isprmidlc  21679  submabas  22948  pmatcollpw3lem  23156  elcls2  23447  isclo2  23461  cmpsublem  23772  cmpsub  23773  hauscmplem  23779  1stcelcls  23835  llyss  23853  nllyss  23854  txkgen  24026  nrmr0reg  24123  uffix  24295  ufinffr  24303  ufilen  24304  fmfnfmlem2  24329  alexsubALTlem2  24422  alexsubALT  24425  metrest  24898  iccntr  25196  reconnlem2  25202  clmneg1  25458  clmvscom  25466  caubl  25684  dvply2g  26661  ulmss  26781  nofv  28071  nocvxminlem  28197  nocvxmin  28198  axcontlem4  29602  ocsh  31942  ococss  31952  shorth  31954  spansnss2  32234  h1datomi  32240  pjss2i  32339  pjssmii  32340  pjorthcoi  32828  pj3si  32866  ssrelf  33307  dfimafnf  33328  funimass4f  33329  mptssALT  33365  1stpreima  33397  2ndpreima  33398  ordtconnlem1  34667  bnj518  35627  nummin  35847  tz9.1regs  35943  cvmlift2lem1  36275  satffunlem2lem1  36377  satfvel  36385  dfon2lem6  36765  limsucncmpi  37448  bj-ssrel  38175  finxpreclem4  38585  poimirlem3  38809  poimirlem29  38835  poimirlem32  38838  ismtyres  39008  ispridlc  39270  iss2  39542  paddss1  41140  paddss2  41141  lspindp5  43093  sn-sup2  43821  sn-sup3d  43822  dffltz  43936  pw2f1ocnv  44310  onsupmaxb  44502  naddwordnexlem2  44661  ss2iundf  44920  iunrelexp0  44963  gneispace0nelrn3  45403  nzss  45562  onfrALTlem3  45787  onfrALTlem2  45789  sspwtr  46063  sspwtrALT  46064  sspwtrALT2  46065  pwtrVD  46066  pwtrrVD  46067  suctrALT2VD  46078  suctrALT2  46079  onfrALTlem3VD  46129  onfrALTlem2VD  46131  relpmin  46206  relpfrlem  46207  ssclaxsep  46236  omssaxinf2  46242  iinssf  46426  qndenserrnopnlem  47580  dfaimafn  48508  sprsymrelfolem2  48848  mgmplusfreseq  49535  gsumlsscl  49823  lincfsuppcl  49856  linccl  49857  onsetrec  51207