Theorem ssel 3150

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1351   = wceq 1353  ∃wex 1492   ∈ wcel 2148   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  ssel2  3151  sseli  3152  sseld  3155  sstr2  3163  nelss  3217  ssrexf  3218  ssralv  3220  ssrexv  3221  ralss  3222  rexss  3223  ssconb  3269  sscon  3270  ssdif  3271  unss1  3305  ssrin  3361  difin2  3398  reuss2  3416  reupick  3420  sssnm  3755  uniss  3831  ss2iun  3902  ssiun  3929  iinss  3939  disjss2  3984  disjss1  3987  pwnss  4160  sspwb  4217  ssopab2b  4277  soss  4315  sucssel  4425  ssorduni  4487  onintonm  4517  onnmin  4568  ssnel  4569  wessep  4578  ssrel  4715  ssrel2  4717  ssrelrel  4727  xpss12  4734  cnvss  4801  dmss  4827  elreldm  4854  dmcosseq  4899  relssres  4946  iss  4954  resopab2  4955  issref  5012  ssrnres  5072  dfco2a  5130  cores  5133  funssres  5259  fununi  5285  funimaexglem  5300  dfimafn  5565  funimass4  5567  funimass3  5633  dff4im  5663  funfvima2  5750  funfvima3  5751  f1elima  5774  riotass2  5857  ssoprab2b  5932  resoprab2  5972  releldm2  6186  reldmtpos  6254  dmtpos  6257  rdgss  6384  ss2ixp  6711  fiintim  6928  negf1o  8339  lbreu  8902  lbinf  8905  eqreznegel  9614  negm  9615  iccsupr  9966  negfi  11236  sumrbdclem  11385  prodrbdclem  11579  fprodmodd  11649  mulgpropdg  13025  subgintm  13058  subrgintm  13364  metrest  14009  bdop  14630  bj-nnen2lp  14709  exmidsbthrlem  14773