Theorem ssel 3232

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2203   ⊆ wss 3211

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  ssel2  3233  sseli  3234  sseld  3237  sstr2  3245  nelss  3299  ssrexf  3300  ssralv  3302  ssrexv  3303  ralss  3304  rexss  3305  ssconb  3352  sscon  3353  ssdif  3354  unss1  3388  ssrin  3446  difin2  3483  reuss2  3501  reupick  3505  sssnm  3858  uniss  3935  ss2iun  4006  ssiun  4033  iinss  4043  disjss2  4088  disjss1  4091  pwnss  4272  sspwb  4332  ssopab2b  4395  soss  4435  sucssel  4545  ssorduni  4609  onintonm  4639  onnmin  4690  ssnel  4691  wessep  4700  ssrel  4838  ssrel2  4840  ssrelrel  4850  xpss12  4857  cnvss  4928  dmss  4955  elreldm  4983  dmcosseq  5029  relssres  5076  iss  5084  resopab2  5085  issref  5145  ssrnres  5205  dfco2a  5263  cores  5266  funssres  5395  fununi  5424  funimaexglem  5439  dfimafn  5725  funimass4  5727  funimass3  5794  dff4im  5823  funfvima2  5919  funfvima3  5920  f1elima  5946  riotass2  6032  ssoprab2b  6110  resoprab2  6150  relmptopab  6256  releldm2  6379  reldmtpos  6484  dmtpos  6487  rdgss  6614  ss2ixp  6946  1ndom2  7119  fiintim  7191  negf1o  8655  lbreu  9219  lbinf  9222  eqreznegel  9946  negm  9947  iccsupr  10299  negfi  11913  sumrbdclem  12063  prodrbdclem  12257  fprodmodd  12327  mulgpropdg  13881  subgintm  13915  subrngintm  14357  subrgintm  14388  islssm  14505  lspsnel6  14556  islidlm  14627  metrest  15371  bdop  16645  bj-nnen2lp  16724  exmidsbthrlem  16802