Theorem ssel 3086

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

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1329   = wceq 1331  ∃wex 1468   ∈ wcel 1480   ⊆ wss 3066

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  ssel2  3087  sseli  3088  sseld  3091  sstr2  3099  nelss  3153  ssrexf  3154  ssralv  3156  ssrexv  3157  ralss  3158  rexss  3159  ssconb  3204  sscon  3205  ssdif  3206  unss1  3240  ssrin  3296  difin2  3333  reuss2  3351  reupick  3355  sssnm  3676  uniss  3752  ss2iun  3823  ssiun  3850  iinss  3859  disjss2  3904  disjss1  3907  pwnss  4078  sspwb  4133  ssopab2b  4193  soss  4231  sucssel  4341  ssorduni  4398  onintonm  4428  onnmin  4478  ssnel  4479  wessep  4487  ssrel  4622  ssrel2  4624  ssrelrel  4634  xpss12  4641  cnvss  4707  dmss  4733  elreldm  4760  dmcosseq  4805  relssres  4852  iss  4860  resopab2  4861  issref  4916  ssrnres  4976  dfco2a  5034  cores  5037  funssres  5160  fununi  5186  funimaexglem  5201  dfimafn  5463  funimass4  5465  funimass3  5529  dff4im  5559  funfvima2  5643  funfvima3  5644  f1elima  5667  riotass2  5749  ssoprab2b  5821  resoprab2  5861  releldm2  6076  reldmtpos  6143  dmtpos  6146  rdgss  6273  ss2ixp  6598  fiintim  6810  negf1o  8137  lbreu  8696  lbinf  8699  eqreznegel  9399  negm  9400  iccsupr  9742  negfi  10992  sumrbdclem  11138  prodrbdclem  11333  metrest  12664  bdop  13062  bj-nnen2lp  13141  exmidsbthrlem  13206