Theorem ssel 3191

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1371   = wceq 1373  ∃wex 1516   ∈ wcel 2177   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  ssel2  3192  sseli  3193  sseld  3196  sstr2  3204  nelss  3258  ssrexf  3259  ssralv  3261  ssrexv  3262  ralss  3263  rexss  3264  ssconb  3310  sscon  3311  ssdif  3312  unss1  3346  ssrin  3402  difin2  3439  reuss2  3457  reupick  3461  sssnm  3803  uniss  3880  ss2iun  3951  ssiun  3978  iinss  3988  disjss2  4033  disjss1  4036  pwnss  4214  sspwb  4273  ssopab2b  4336  soss  4374  sucssel  4484  ssorduni  4548  onintonm  4578  onnmin  4629  ssnel  4630  wessep  4639  ssrel  4776  ssrel2  4778  ssrelrel  4788  xpss12  4795  cnvss  4864  dmss  4891  elreldm  4918  dmcosseq  4964  relssres  5011  iss  5019  resopab2  5020  issref  5079  ssrnres  5139  dfco2a  5197  cores  5200  funssres  5327  fununi  5356  funimaexglem  5371  dfimafn  5645  funimass4  5647  funimass3  5714  dff4im  5744  funfvima2  5835  funfvima3  5836  f1elima  5860  riotass2  5944  ssoprab2b  6020  resoprab2  6060  releldm2  6289  reldmtpos  6357  dmtpos  6360  rdgss  6487  ss2ixp  6816  1ndom2  6982  fiintim  7049  negf1o  8484  lbreu  9048  lbinf  9051  eqreznegel  9765  negm  9766  iccsupr  10118  negfi  11624  sumrbdclem  11773  prodrbdclem  11967  fprodmodd  12037  mulgpropdg  13585  subgintm  13619  subrngintm  14059  subrgintm  14090  islssm  14204  lspsnel6  14255  islidlm  14326  metrest  15063  bdop  15980  bj-nnen2lp  16059  exmidsbthrlem  16133