Theorem ssel 3033

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 3028	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	biimpi 119	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	19.21bi 1502	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	3	anim2d 331	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	eximdv 1815	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		df-clel 2091	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2091	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3imtr4g 204	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1294   = wceq 1296  ∃wex 1433   ∈ wcel 1445   ⊆ wss 3013

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-in 3019  df-ss 3026

This theorem is referenced by:  ssel2  3034  sseli  3035  sseld  3038  sstr2  3046  ssralv  3100  ssrexv  3101  ralss  3102  rexss  3103  ssconb  3148  sscon  3149  ssdif  3150  unss1  3184  ssrin  3240  difin2  3277  reuss2  3295  reupick  3299  sssnm  3620  uniss  3696  ss2iun  3767  ssiun  3794  iinss  3803  disjss2  3847  disjss1  3850  pwnss  4015  sspwb  4067  ssopab2b  4127  soss  4165  sucssel  4275  ssorduni  4332  onintonm  4362  onnmin  4412  ssnel  4413  wessep  4421  ssrel  4555  ssrel2  4557  ssrelrel  4567  xpss12  4574  cnvss  4640  dmss  4666  elreldm  4693  dmcosseq  4736  relssres  4783  iss  4791  resopab2  4792  issref  4847  ssrnres  4907  dfco2a  4965  cores  4968  funssres  5090  fununi  5116  funimaexglem  5131  dfimafn  5388  funimass4  5390  funimass3  5454  dff4im  5484  funfvima2  5566  funfvima3  5567  f1elima  5590  riotass2  5672  ssoprab2b  5744  resoprab2  5780  releldm2  5993  reldmtpos  6056  dmtpos  6059  rdgss  6186  ss2ixp  6508  fiintim  6719  negf1o  7957  lbreu  8503  lbinf  8506  eqreznegel  9198  negm  9199  iccsupr  9532  negfi  10790  sumrbdclem  10935  metrest  12308  bdop  12490  bj-nnen2lp  12573  exmidsbthrlem  12633