Theorem ssel 3186

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1370   = wceq 1372  ∃wex 1514   ∈ wcel 2175   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  ssel2  3187  sseli  3188  sseld  3191  sstr2  3199  nelss  3253  ssrexf  3254  ssralv  3256  ssrexv  3257  ralss  3258  rexss  3259  ssconb  3305  sscon  3306  ssdif  3307  unss1  3341  ssrin  3397  difin2  3434  reuss2  3452  reupick  3456  sssnm  3794  uniss  3870  ss2iun  3941  ssiun  3968  iinss  3978  disjss2  4023  disjss1  4026  pwnss  4202  sspwb  4259  ssopab2b  4322  soss  4360  sucssel  4470  ssorduni  4534  onintonm  4564  onnmin  4615  ssnel  4616  wessep  4625  ssrel  4762  ssrel2  4764  ssrelrel  4774  xpss12  4781  cnvss  4850  dmss  4876  elreldm  4903  dmcosseq  4949  relssres  4996  iss  5004  resopab2  5005  issref  5064  ssrnres  5124  dfco2a  5182  cores  5185  funssres  5312  fununi  5341  funimaexglem  5356  dfimafn  5626  funimass4  5628  funimass3  5695  dff4im  5725  funfvima2  5816  funfvima3  5817  f1elima  5841  riotass2  5925  ssoprab2b  6001  resoprab2  6041  releldm2  6270  reldmtpos  6338  dmtpos  6341  rdgss  6468  ss2ixp  6797  fiintim  7027  negf1o  8453  lbreu  9017  lbinf  9020  eqreznegel  9734  negm  9735  iccsupr  10087  negfi  11481  sumrbdclem  11630  prodrbdclem  11824  fprodmodd  11894  mulgpropdg  13442  subgintm  13476  subrngintm  13916  subrgintm  13947  islssm  14061  lspsnel6  14112  islidlm  14183  metrest  14920  bdop  15744  bj-nnen2lp  15823  exmidsbthrlem  15894