Theorem ssel 3151

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1351   = wceq 1353  ∃wex 1492   ∈ wcel 2148   ⊆ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  ssel2  3152  sseli  3153  sseld  3156  sstr2  3164  nelss  3218  ssrexf  3219  ssralv  3221  ssrexv  3222  ralss  3223  rexss  3224  ssconb  3270  sscon  3271  ssdif  3272  unss1  3306  ssrin  3362  difin2  3399  reuss2  3417  reupick  3421  sssnm  3756  uniss  3832  ss2iun  3903  ssiun  3930  iinss  3940  disjss2  3985  disjss1  3988  pwnss  4161  sspwb  4218  ssopab2b  4278  soss  4316  sucssel  4426  ssorduni  4488  onintonm  4518  onnmin  4569  ssnel  4570  wessep  4579  ssrel  4716  ssrel2  4718  ssrelrel  4728  xpss12  4735  cnvss  4802  dmss  4828  elreldm  4855  dmcosseq  4900  relssres  4947  iss  4955  resopab2  4956  issref  5013  ssrnres  5073  dfco2a  5131  cores  5134  funssres  5260  fununi  5286  funimaexglem  5301  dfimafn  5566  funimass4  5568  funimass3  5634  dff4im  5664  funfvima2  5751  funfvima3  5752  f1elima  5776  riotass2  5859  ssoprab2b  5934  resoprab2  5974  releldm2  6188  reldmtpos  6256  dmtpos  6259  rdgss  6386  ss2ixp  6713  fiintim  6930  negf1o  8341  lbreu  8904  lbinf  8907  eqreznegel  9616  negm  9617  iccsupr  9968  negfi  11238  sumrbdclem  11387  prodrbdclem  11581  fprodmodd  11651  mulgpropdg  13030  subgintm  13063  subrgintm  13369  lspsnel6  13499  metrest  14091  bdop  14712  bj-nnen2lp  14791  exmidsbthrlem  14855