Theorem ssel 3221

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1395   = wceq 1397  ∃wex 1540   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  ssel2  3222  sseli  3223  sseld  3226  sstr2  3234  nelss  3288  ssrexf  3289  ssralv  3291  ssrexv  3292  ralss  3293  rexss  3294  ssconb  3340  sscon  3341  ssdif  3342  unss1  3376  ssrin  3432  difin2  3469  reuss2  3487  reupick  3491  sssnm  3837  uniss  3914  ss2iun  3985  ssiun  4012  iinss  4022  disjss2  4067  disjss1  4070  pwnss  4249  sspwb  4308  ssopab2b  4371  soss  4411  sucssel  4521  ssorduni  4585  onintonm  4615  onnmin  4666  ssnel  4667  wessep  4676  ssrel  4814  ssrel2  4816  ssrelrel  4826  xpss12  4833  cnvss  4903  dmss  4930  elreldm  4958  dmcosseq  5004  relssres  5051  iss  5059  resopab2  5060  issref  5119  ssrnres  5179  dfco2a  5237  cores  5240  funssres  5369  fununi  5398  funimaexglem  5413  dfimafn  5694  funimass4  5696  funimass3  5763  dff4im  5793  funfvima2  5887  funfvima3  5888  f1elima  5914  riotass2  6000  ssoprab2b  6078  resoprab2  6118  relmptopab  6224  releldm2  6348  reldmtpos  6419  dmtpos  6422  rdgss  6549  ss2ixp  6880  1ndom2  7051  fiintim  7123  negf1o  8561  lbreu  9125  lbinf  9128  eqreznegel  9848  negm  9849  iccsupr  10201  negfi  11793  sumrbdclem  11943  prodrbdclem  12137  fprodmodd  12207  mulgpropdg  13756  subgintm  13790  subrngintm  14232  subrgintm  14263  islssm  14377  lspsnel6  14428  islidlm  14499  metrest  15236  bdop  16496  bj-nnen2lp  16575  exmidsbthrlem  16652