Theorem ssel 3177

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1362   = wceq 1364  ∃wex 1506   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  ssel2  3178  sseli  3179  sseld  3182  sstr2  3190  nelss  3244  ssrexf  3245  ssralv  3247  ssrexv  3248  ralss  3249  rexss  3250  ssconb  3296  sscon  3297  ssdif  3298  unss1  3332  ssrin  3388  difin2  3425  reuss2  3443  reupick  3447  sssnm  3784  uniss  3860  ss2iun  3931  ssiun  3958  iinss  3968  disjss2  4013  disjss1  4016  pwnss  4192  sspwb  4249  ssopab2b  4311  soss  4349  sucssel  4459  ssorduni  4523  onintonm  4553  onnmin  4604  ssnel  4605  wessep  4614  ssrel  4751  ssrel2  4753  ssrelrel  4763  xpss12  4770  cnvss  4839  dmss  4865  elreldm  4892  dmcosseq  4937  relssres  4984  iss  4992  resopab2  4993  issref  5052  ssrnres  5112  dfco2a  5170  cores  5173  funssres  5300  fununi  5326  funimaexglem  5341  dfimafn  5609  funimass4  5611  funimass3  5678  dff4im  5708  funfvima2  5795  funfvima3  5796  f1elima  5820  riotass2  5904  ssoprab2b  5979  resoprab2  6019  releldm2  6243  reldmtpos  6311  dmtpos  6314  rdgss  6441  ss2ixp  6770  fiintim  6992  negf1o  8408  lbreu  8972  lbinf  8975  eqreznegel  9688  negm  9689  iccsupr  10041  negfi  11393  sumrbdclem  11542  prodrbdclem  11736  fprodmodd  11806  mulgpropdg  13294  subgintm  13328  subrngintm  13768  subrgintm  13799  islssm  13913  lspsnel6  13964  islidlm  14035  metrest  14742  bdop  15521  bj-nnen2lp  15600  exmidsbthrlem  15666