Theorem ssel 3178

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1362   = wceq 1364  ∃wex 1506   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  ssel2  3179  sseli  3180  sseld  3183  sstr2  3191  nelss  3245  ssrexf  3246  ssralv  3248  ssrexv  3249  ralss  3250  rexss  3251  ssconb  3297  sscon  3298  ssdif  3299  unss1  3333  ssrin  3389  difin2  3426  reuss2  3444  reupick  3448  sssnm  3785  uniss  3861  ss2iun  3932  ssiun  3959  iinss  3969  disjss2  4014  disjss1  4017  pwnss  4193  sspwb  4250  ssopab2b  4312  soss  4350  sucssel  4460  ssorduni  4524  onintonm  4554  onnmin  4605  ssnel  4606  wessep  4615  ssrel  4752  ssrel2  4754  ssrelrel  4764  xpss12  4771  cnvss  4840  dmss  4866  elreldm  4893  dmcosseq  4938  relssres  4985  iss  4993  resopab2  4994  issref  5053  ssrnres  5113  dfco2a  5171  cores  5174  funssres  5301  fununi  5327  funimaexglem  5342  dfimafn  5612  funimass4  5614  funimass3  5681  dff4im  5711  funfvima2  5798  funfvima3  5799  f1elima  5823  riotass2  5907  ssoprab2b  5983  resoprab2  6023  releldm2  6252  reldmtpos  6320  dmtpos  6323  rdgss  6450  ss2ixp  6779  fiintim  7001  negf1o  8427  lbreu  8991  lbinf  8994  eqreznegel  9707  negm  9708  iccsupr  10060  negfi  11412  sumrbdclem  11561  prodrbdclem  11755  fprodmodd  11825  mulgpropdg  13372  subgintm  13406  subrngintm  13846  subrgintm  13877  islssm  13991  lspsnel6  14042  islidlm  14113  metrest  14850  bdop  15629  bj-nnen2lp  15708  exmidsbthrlem  15779