Theorem ssel 3236

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2205   ⊆ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  ssel2  3237  sseli  3238  sseld  3241  sstr2  3249  nelss  3303  ssrexf  3304  ssralv  3306  ssrexv  3307  ralss  3308  rexss  3309  ssconb  3356  sscon  3357  ssdif  3358  unss1  3392  ssrin  3450  difin2  3487  reuss2  3505  reupick  3509  sssnm  3863  uniss  3940  ss2iun  4011  ssiun  4038  iinss  4048  disjss2  4093  disjss1  4096  pwnss  4277  sspwb  4337  ssopab2b  4400  soss  4440  sucssel  4550  ssorduni  4614  onintonm  4644  onnmin  4695  ssnel  4696  wessep  4705  ssrel  4843  ssrel2  4845  ssrelrel  4855  xpss12  4862  cnvss  4933  dmss  4960  elreldm  4988  dmcosseq  5034  relssres  5081  iss  5089  resopab2  5090  issref  5150  ssrnres  5210  dfco2a  5268  cores  5271  funssres  5400  fununi  5429  funimaexglem  5444  dfimafn  5730  funimass4  5732  funimass3  5799  dff4im  5828  funfvima2  5924  funfvima3  5925  dfimafnf  5928  f1elima  5952  riotass2  6040  ssoprab2b  6118  resoprab2  6158  relmptopab  6264  funimass4f  6332  releldm2  6392  reldmtpos  6497  dmtpos  6500  rdgss  6627  ss2ixp  6959  1ndom2  7132  fiintim  7204  negf1o  8672  lbreu  9236  lbinf  9239  eqreznegel  9964  negm  9965  iccsupr  10318  negfi  11938  sumrbdclem  12088  prodrbdclem  12282  fprodmodd  12352  mulgpropdg  13917  subgintm  13951  subrngintm  14458  subrgintm  14489  islssm  14631  lspsnel6  14682  islidlm  14753  metrest  15497  bdop  16771  bj-nnen2lp  16850  exmidsbthrlem  16928