Theorem ssel 3136

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 3131	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	biimpi 119	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	19.21bi 1546	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	3	anim2d 335	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	eximdv 1868	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		df-clel 2161	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2161	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3imtr4g 204	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1341   = wceq 1343  ∃wex 1480   ∈ wcel 2136   ⊆ wss 3116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129

This theorem is referenced by:  ssel2  3137  sseli  3138  sseld  3141  sstr2  3149  nelss  3203  ssrexf  3204  ssralv  3206  ssrexv  3207  ralss  3208  rexss  3209  ssconb  3255  sscon  3256  ssdif  3257  unss1  3291  ssrin  3347  difin2  3384  reuss2  3402  reupick  3406  sssnm  3734  uniss  3810  ss2iun  3881  ssiun  3908  iinss  3917  disjss2  3962  disjss1  3965  pwnss  4138  sspwb  4194  ssopab2b  4254  soss  4292  sucssel  4402  ssorduni  4464  onintonm  4494  onnmin  4545  ssnel  4546  wessep  4555  ssrel  4692  ssrel2  4694  ssrelrel  4704  xpss12  4711  cnvss  4777  dmss  4803  elreldm  4830  dmcosseq  4875  relssres  4922  iss  4930  resopab2  4931  issref  4986  ssrnres  5046  dfco2a  5104  cores  5107  funssres  5230  fununi  5256  funimaexglem  5271  dfimafn  5535  funimass4  5537  funimass3  5601  dff4im  5631  funfvima2  5717  funfvima3  5718  f1elima  5741  riotass2  5824  ssoprab2b  5899  resoprab2  5939  releldm2  6153  reldmtpos  6221  dmtpos  6224  rdgss  6351  ss2ixp  6677  fiintim  6894  negf1o  8280  lbreu  8840  lbinf  8843  eqreznegel  9552  negm  9553  iccsupr  9902  negfi  11169  sumrbdclem  11318  prodrbdclem  11512  fprodmodd  11582  metrest  13156  bdop  13767  bj-nnen2lp  13846  exmidsbthrlem  13911