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  5886  funfvima3  5887  f1elima  5913  riotass2  5999  ssoprab2b  6077  resoprab2  6117  relmptopab  6223  releldm2  6347  reldmtpos  6418  dmtpos  6421  rdgss  6548  ss2ixp  6879  1ndom2  7050  fiintim  7122  negf1o  8560  lbreu  9124  lbinf  9127  eqreznegel  9847  negm  9848  iccsupr  10200  negfi  11788  sumrbdclem  11937  prodrbdclem  12131  fprodmodd  12201  mulgpropdg  13750  subgintm  13784  subrngintm  14225  subrgintm  14256  islssm  14370  lspsnel6  14421  islidlm  14492  metrest  15229  bdop  16470  bj-nnen2lp  16549  exmidsbthrlem  16626