Theorem ssel 3174

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2164   ⊆ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  ssel2  3175  sseli  3176  sseld  3179  sstr2  3187  nelss  3241  ssrexf  3242  ssralv  3244  ssrexv  3245  ralss  3246  rexss  3247  ssconb  3293  sscon  3294  ssdif  3295  unss1  3329  ssrin  3385  difin2  3422  reuss2  3440  reupick  3444  sssnm  3781  uniss  3857  ss2iun  3928  ssiun  3955  iinss  3965  disjss2  4010  disjss1  4013  pwnss  4189  sspwb  4246  ssopab2b  4308  soss  4346  sucssel  4456  ssorduni  4520  onintonm  4550  onnmin  4601  ssnel  4602  wessep  4611  ssrel  4748  ssrel2  4750  ssrelrel  4760  xpss12  4767  cnvss  4836  dmss  4862  elreldm  4889  dmcosseq  4934  relssres  4981  iss  4989  resopab2  4990  issref  5049  ssrnres  5109  dfco2a  5167  cores  5170  funssres  5297  fununi  5323  funimaexglem  5338  dfimafn  5606  funimass4  5608  funimass3  5675  dff4im  5705  funfvima2  5792  funfvima3  5793  f1elima  5817  riotass2  5901  ssoprab2b  5976  resoprab2  6016  releldm2  6240  reldmtpos  6308  dmtpos  6311  rdgss  6438  ss2ixp  6767  fiintim  6987  negf1o  8403  lbreu  8966  lbinf  8969  eqreznegel  9682  negm  9683  iccsupr  10035  negfi  11374  sumrbdclem  11523  prodrbdclem  11717  fprodmodd  11787  mulgpropdg  13237  subgintm  13271  subrngintm  13711  subrgintm  13742  islssm  13856  lspsnel6  13907  islidlm  13978  metrest  14685  bdop  15437  bj-nnen2lp  15516  exmidsbthrlem  15582