Theorem ssel 3222

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  ssel2  3223  sseli  3224  sseld  3227  sstr2  3235  nelss  3289  ssrexf  3290  ssralv  3292  ssrexv  3293  ralss  3294  rexss  3295  ssconb  3342  sscon  3343  ssdif  3344  unss1  3378  ssrin  3434  difin2  3471  reuss2  3489  reupick  3493  sssnm  3842  uniss  3919  ss2iun  3990  ssiun  4017  iinss  4027  disjss2  4072  disjss1  4075  pwnss  4255  sspwb  4314  ssopab2b  4377  soss  4417  sucssel  4527  ssorduni  4591  onintonm  4621  onnmin  4672  ssnel  4673  wessep  4682  ssrel  4820  ssrel2  4822  ssrelrel  4832  xpss12  4839  cnvss  4909  dmss  4936  elreldm  4964  dmcosseq  5010  relssres  5057  iss  5065  resopab2  5066  issref  5126  ssrnres  5186  dfco2a  5244  cores  5247  funssres  5376  fununi  5405  funimaexglem  5420  dfimafn  5703  funimass4  5705  funimass3  5772  dff4im  5801  funfvima2  5897  funfvima3  5898  f1elima  5924  riotass2  6010  ssoprab2b  6088  resoprab2  6128  relmptopab  6234  releldm2  6357  reldmtpos  6462  dmtpos  6465  rdgss  6592  ss2ixp  6923  1ndom2  7094  fiintim  7166  negf1o  8603  lbreu  9167  lbinf  9170  eqreznegel  9892  negm  9893  iccsupr  10245  negfi  11851  sumrbdclem  12001  prodrbdclem  12195  fprodmodd  12265  mulgpropdg  13814  subgintm  13848  subrngintm  14290  subrgintm  14321  islssm  14436  lspsnel6  14487  islidlm  14558  metrest  15300  bdop  16574  bj-nnen2lp  16653  exmidsbthrlem  16733