Theorem ssel 3219

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 3213	. . . . . 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 3198

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 3204  df-ss 3211

This theorem is referenced by:  ssel2  3220  sseli  3221  sseld  3224  sstr2  3232  nelss  3286  ssrexf  3287  ssralv  3289  ssrexv  3290  ralss  3291  rexss  3292  ssconb  3338  sscon  3339  ssdif  3340  unss1  3374  ssrin  3430  difin2  3467  reuss2  3485  reupick  3489  sssnm  3835  uniss  3912  ss2iun  3983  ssiun  4010  iinss  4020  disjss2  4065  disjss1  4068  pwnss  4247  sspwb  4306  ssopab2b  4369  soss  4409  sucssel  4519  ssorduni  4583  onintonm  4613  onnmin  4664  ssnel  4665  wessep  4674  ssrel  4812  ssrel2  4814  ssrelrel  4824  xpss12  4831  cnvss  4901  dmss  4928  elreldm  4956  dmcosseq  5002  relssres  5049  iss  5057  resopab2  5058  issref  5117  ssrnres  5177  dfco2a  5235  cores  5238  funssres  5366  fununi  5395  funimaexglem  5410  dfimafn  5690  funimass4  5692  funimass3  5759  dff4im  5789  funfvima2  5882  funfvima3  5883  f1elima  5909  riotass2  5995  ssoprab2b  6073  resoprab2  6113  relmptopab  6219  releldm2  6343  reldmtpos  6414  dmtpos  6417  rdgss  6544  ss2ixp  6875  1ndom2  7046  fiintim  7116  negf1o  8551  lbreu  9115  lbinf  9118  eqreznegel  9838  negm  9839  iccsupr  10191  negfi  11779  sumrbdclem  11928  prodrbdclem  12122  fprodmodd  12192  mulgpropdg  13741  subgintm  13775  subrngintm  14216  subrgintm  14247  islssm  14361  lspsnel6  14412  islidlm  14483  metrest  15220  bdop  16406  bj-nnen2lp  16485  exmidsbthrlem  16562