Theorem ssel 3959

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem ssel

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfss2 3953	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	biimpi 218	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	19.21bi 2181	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	3	anim2d 613	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	eximdv 1912	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		dfclel 2892	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		dfclel 2892	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3imtr4g 298	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 398  ∀wal 1529   = wceq 1531  ∃wex 1774   ∈ wcel 2108   ⊆ wss 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950

This theorem is referenced by:  ssel2  3960  sseli  3961  sseld  3964  sstr2  3972  nelss  4028  ssrexf  4029  ssralv  4031  ssrexv  4032  ralss  4035  rexss  4036  ssconb  4112  sscon  4113  ssdif  4114  unss1  4153  ssrin  4208  difin2  4264  reuss2  4281  reupick  4285  elpwunsn  4613  sssn  4751  uniss  4851  ss2iun  4928  ssiun  4961  iinss  4971  disjss2  5025  disjss1  5028  pwnss  5241  sspwb  5332  ssopab2bw  5425  ssopab2b  5427  pwssun  5448  xpss12  5563  frinxp  5627  ssrel  5650  ssrel2  5652  ssrelrel  5662  dmss  5764  elreldm  5798  dmcosseq  5837  relssres  5886  iss  5896  resopab2  5897  ssrnres  6028  dfco2a  6092  cores  6095  oneqmini  6235  sucssel  6276  onssneli  6293  onssnel2i  6294  funssres  6391  fununi  6422  dfimafn  6721  funimass4  6723  funimass3  6817  dff3  6859  dff4  6860  funfvima2  6985  funfvima3  6990  f1elima  7013  isomin  7082  isofrlem  7085  riotass2  7136  ssoprab2b  7215  eqoprab2bw  7216  resoprab2  7263  ssorduni  7492  onint  7502  oninton  7507  ssnlim  7591  releldm2  7734  dmtpos  7896  wfrlem10  7956  onfununi  7970  tz7.48lem  8069  tz7.49  8073  omeulem1  8200  omeulem2  8201  omsmolem  8272  omsmo  8273  ss2ixp  8466  boxriin  8496  onomeneq  8700  unblem1  8762  unblem3  8764  fiint  8787  inf3lem2  9084  cantnflem2  9145  tcel  9179  tz9.13  9212  rankr1ag  9223  rankpwi  9244  rankelb  9245  bndrank  9262  cardlim  9393  carduni  9402  acni2  9464  dfac12r  9564  cfub  9663  cflim2  9677  fin1a2lem9  9822  axdc3lem2  9865  axdclem2  9934  gch2  10089  eltsk2g  10165  suplem1pr  10466  negn0  11061  negf1o  11062  fimaxreOLD  11577  negfi  11581  fiminreOLD  11582  lbreu  11583  lbinf  11586  sup2  11589  sup3  11590  infm3  11592  infregelb  11617  uzwo  12303  eqreznegel  12326  xrsupsslem  12692  xrinfmsslem  12693  supxrpnf  12703  supxrunb1  12704  supxrunb2  12705  iccsupr  12822  ssnn0fi  13345  incexclem  15183  fprodmodd  15343  sumeven  15730  sumodd  15731  gcdcllem1  15840  lcmfnnval  15960  lcmfnncl  15965  dvdslcmf  15967  lcmfunsnlem2lem2  15975  lcmfdvdsb  15979  lubel  17724  clatleglb  17728  smndex1mgm  18064  smndex1sgrp  18065  smndex1mnd  18067  mulgpropd  18261  sylow2a  18736  efgi2  18843  lspsnel6  19758  submabas  21179  pmatcollpw3lem  21383  elcls2  21674  isclo2  21688  cmpsublem  21999  cmpsub  22000  hauscmplem  22006  1stcelcls  22061  llyss  22079  nllyss  22080  txkgen  22252  nrmr0reg  22349  uffix  22521  ufinffr  22529  ufilen  22530  fmfnfmlem2  22555  alexsubALTlem2  22648  alexsubALT  22651  metrest  23126  iccntr  23421  reconnlem2  23427  clmneg1  23678  clmvscom  23686  caubl  23903  ulmss  24977  axcontlem4  26745  ocsh  29052  ococss  29062  shorth  29064  spansnss2  29344  h1datomi  29350  pjss2i  29449  pjssmii  29450  pjorthcoi  29938  pj3si  29976  ssrelf  30358  dfimafnf  30373  funimass4f  30374  mptssALT  30412  1stpreima  30434  2ndpreima  30435  isprmidlc  30956  ordtconnlem1  31160  indpi1  31272  bnj518  32151  cvmlift2lem1  32542  satffunlem2lem1  32644  satfvel  32652  dfon2lem6  33026  trpredmintr  33063  orderseqlem  33087  nofv  33157  nocvxminlem  33240  nocvxmin  33241  limsucncmpi  33786  finxpreclem4  34667  poimirlem3  34887  poimirlem29  34913  poimirlem32  34916  ismtyres  35078  ispridlc  35340  iss2  35593  paddss1  36945  paddss2  36946  lspindp5  38898  dffltz  39261  pw2f1ocnv  39624  ss2iundf  39994  iunrelexp0  40037  gneispace0nelrn3  40482  nzss  40639  onfrALTlem3  40868  onfrALTlem2  40870  sspwtr  41145  sspwtrALT  41146  sspwtrALT2  41147  pwtrVD  41148  pwtrrVD  41149  suctrALT2VD  41160  suctrALT2  41161  onfrALTlem3VD  41211  onfrALTlem2VD  41213  iinssf  41396  qndenserrnopnlem  42572  dfaimafn  43354  sprsymrelfolem2  43645  mgmplusfreseq  44030  gsumlsscl  44421  lincfsuppcl  44458  linccl  44459  onsetrec  44800