Theorem ssel 3218

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1393   = wceq 1395  ∃wex 1538   ∈ wcel 2200   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  ssel2  3219  sseli  3220  sseld  3223  sstr2  3231  nelss  3285  ssrexf  3286  ssralv  3288  ssrexv  3289  ralss  3290  rexss  3291  ssconb  3337  sscon  3338  ssdif  3339  unss1  3373  ssrin  3429  difin2  3466  reuss2  3484  reupick  3488  sssnm  3831  uniss  3908  ss2iun  3979  ssiun  4006  iinss  4016  disjss2  4061  disjss1  4064  pwnss  4242  sspwb  4301  ssopab2b  4364  soss  4404  sucssel  4514  ssorduni  4578  onintonm  4608  onnmin  4659  ssnel  4660  wessep  4669  ssrel  4806  ssrel2  4808  ssrelrel  4818  xpss12  4825  cnvss  4894  dmss  4921  elreldm  4949  dmcosseq  4995  relssres  5042  iss  5050  resopab2  5051  issref  5110  ssrnres  5170  dfco2a  5228  cores  5231  funssres  5359  fununi  5388  funimaexglem  5403  dfimafn  5681  funimass4  5683  funimass3  5750  dff4im  5780  funfvima2  5871  funfvima3  5872  f1elima  5896  riotass2  5982  ssoprab2b  6060  resoprab2  6100  releldm2  6329  reldmtpos  6397  dmtpos  6400  rdgss  6527  ss2ixp  6856  1ndom2  7022  fiintim  7089  negf1o  8524  lbreu  9088  lbinf  9091  eqreznegel  9805  negm  9806  iccsupr  10158  negfi  11734  sumrbdclem  11883  prodrbdclem  12077  fprodmodd  12147  mulgpropdg  13696  subgintm  13730  subrngintm  14170  subrgintm  14201  islssm  14315  lspsnel6  14366  islidlm  14437  metrest  15174  bdop  16196  bj-nnen2lp  16275  exmidsbthrlem  16349