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 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209   ⊆ wss 3220

This proof depends on 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 proof 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 used 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  3879  uniss  3956  ss2iun  4027  ssiun  4054  iinss  4064  disjss2  4109  disjss1  4112  pwnss  4298  sspwb  4358  ssopab2b  4421  soss  4461  sucssel  4571  ssorduni  4636  onintonm  4666  onnmin  4717  ssnel  4718  wessep  4727  ssrel  4865  ssrel2  4867  ssrelrel  4877  xpss12  4884  cnvss  4955  dmss  4982  elreldm  5010  dmcosseq  5056  relssres  5103  iss  5112  resopab2  5113  issref  5173  ssrnres  5233  dfco2a  5291  cores  5294  funssres  5423  fununi  5452  funimaexglem  5467  dfimafn  5754  funimass4  5756  funimass3  5828  dff4im  5857  funfvima2  5954  funfvima3  5955  dfimafnf  5958  f1elima  5982  riotass2  6070  ssoprab2b  6148  resoprab2  6188  relmptopab  6294  funimass4f  6363  releldm2  6423  reldmtpos  6528  dmtpos  6531  rdgss  6658  ss2ixp  6997  1ndom2  7170  fiintim  7242  negf1o  8716  lbreu  9283  lbinf  9286  eqreznegel  10030  negm  10031  iccsupr  10385  negfi  12017  sumrbdclem  12169  prodrbdclem  12363  fprodmodd  12433  mulgpropdg  14026  subgintm  14060  subrngintm  14629  subrgintm  14660  islssm  14803  ellspsn6  14854  islidlm  14925  metrest  15732  bdop  17106  bj-nnen2lp  17185  exmidsbthrlem  17273