Theorem ssel 3141

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

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1346   = wceq 1348  ∃wex 1485   ∈ wcel 2141   ⊆ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  ssel2  3142  sseli  3143  sseld  3146  sstr2  3154  nelss  3208  ssrexf  3209  ssralv  3211  ssrexv  3212  ralss  3213  rexss  3214  ssconb  3260  sscon  3261  ssdif  3262  unss1  3296  ssrin  3352  difin2  3389  reuss2  3407  reupick  3411  sssnm  3741  uniss  3817  ss2iun  3888  ssiun  3915  iinss  3924  disjss2  3969  disjss1  3972  pwnss  4145  sspwb  4201  ssopab2b  4261  soss  4299  sucssel  4409  ssorduni  4471  onintonm  4501  onnmin  4552  ssnel  4553  wessep  4562  ssrel  4699  ssrel2  4701  ssrelrel  4711  xpss12  4718  cnvss  4784  dmss  4810  elreldm  4837  dmcosseq  4882  relssres  4929  iss  4937  resopab2  4938  issref  4993  ssrnres  5053  dfco2a  5111  cores  5114  funssres  5240  fununi  5266  funimaexglem  5281  dfimafn  5545  funimass4  5547  funimass3  5612  dff4im  5642  funfvima2  5728  funfvima3  5729  f1elima  5752  riotass2  5835  ssoprab2b  5910  resoprab2  5950  releldm2  6164  reldmtpos  6232  dmtpos  6235  rdgss  6362  ss2ixp  6689  fiintim  6906  negf1o  8301  lbreu  8861  lbinf  8864  eqreznegel  9573  negm  9574  iccsupr  9923  negfi  11191  sumrbdclem  11340  prodrbdclem  11534  fprodmodd  11604  metrest  13300  bdop  13910  bj-nnen2lp  13989  exmidsbthrlem  14054