Theorem ssel 3242

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		ssalel 3235	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	biimpi 120	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	19.21bi 1611	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	3	anim2d 337	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	eximdv 1933	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		df-clel 2234	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2234	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3imtr4g 205	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209   ⊆ wss 3220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  ssel2  3243  sseli  3244  sseld  3247  sstr2  3255  nelss  3309  ssrexf  3310  ssralv  3312  ssrexv  3313  ralss  3314  rexss  3315  ssconb  3362  sscon  3363  ssdif  3364  unss1  3398  ssrin  3456  difin2  3493  reuss2  3513  reupick  3517  sssnm  3874  uniss  3951  ss2iun  4022  ssiun  4049  iinss  4059  disjss2  4104  disjss1  4107  pwnss  4291  sspwb  4351  ssopab2b  4414  soss  4454  sucssel  4564  ssorduni  4629  onintonm  4659  onnmin  4710  ssnel  4711  wessep  4720  ssrel  4858  ssrel2  4860  ssrelrel  4870  xpss12  4877  cnvss  4948  dmss  4975  elreldm  5003  dmcosseq  5049  relssres  5096  iss  5104  resopab2  5105  issref  5165  ssrnres  5225  dfco2a  5283  cores  5286  funssres  5415  fununi  5444  funimaexglem  5459  dfimafn  5745  funimass4  5747  funimass3  5816  dff4im  5845  funfvima2  5941  funfvima3  5942  dfimafnf  5945  f1elima  5969  riotass2  6057  ssoprab2b  6135  resoprab2  6175  relmptopab  6281  funimass4f  6349  releldm2  6409  reldmtpos  6514  dmtpos  6517  rdgss  6644  ss2ixp  6983  1ndom2  7156  fiintim  7228  negf1o  8699  lbreu  9265  lbinf  9268  eqreznegel  9993  negm  9994  iccsupr  10347  negfi  11972  sumrbdclem  12122  prodrbdclem  12316  fprodmodd  12386  mulgpropdg  13944  subgintm  13978  subrngintm  14493  subrgintm  14524  islssm  14666  lspsnel6  14717  islidlm  14788  metrest  15530  bdop  16815  bj-nnen2lp  16894  exmidsbthrlem  16972