Theorem sseldd 2620

Description: Membership inference from subclass relationship.

Hypotheses

Ref	Expression
sseld.1	|- (ph -> A C_ B)
sseldd.2	|- (ph -> C e. A)

Assertion

Ref	Expression
sseldd	|- (ph -> C e. B)

Proof of Theorem sseldd

Step	Hyp	Ref	Expression
1		sseldd.2	. 2 |- (ph -> C e. A)
2		sseld.1	. . 3 |- (ph -> A C_ B)
3	2	sseld 2619	. 2 |- (ph -> (C e. A -> C e. B))
4	1, 3	mpd 29	1 |- (ph -> C e. B)

Syntax hints:   -> wi 3   e. wcel 1300   C_ wss 2593

This theorem is referenced by:  reiotacl 5106  omordi 5245  ordtypelem6 5689  ordtypelem7 5690  tz9.12lem3 5772  fzelp1 7681  seqzcl 7801  fsum0diag2 8521  acdc3lem 8754  acdc2lem1 8757  acdc5lem1 8760  acdclem 8763  iooretop 8929  metidcn 9178  bcthlem19 9295  bcthlem27 9303  subgid 9429  ssga 9455  sspz 9733  tx1cn 10223  tx2cn 10224  subtopmetlem 10255  subtopmet 10256  fbssint 10279  fbunfip 10282  extbas1 10291  elfilmap 10312  pjhcl 10876  shatomistici 11933  sumdmdlem2 11991  bnj1213 12986  bnj907 13381  bnj1121 13421  bnj1128 13428  bnj1175 13443  bnj1177 13445  bnj1417 13530  inacint 15221  tarsin 15230  finsschain 15373  ordtypelem6OLD 15380  ordtypelem7OLD 15381  alexsublem3 15439  alexsublem4 15440  reconnlem2 15447  reconnlem4 15449  reconnlem5 15450  ivthALT 15454  2ndcctbss 15478  neibastop2 15523  neibastop3 15524  filfinnfr 15561  isufil2 15565  filssufillem 15570  filssufil 15571  ufileu 15573  filufint 15574  ufinffr 15578  ufilen 15579  flimcls 15588  cnpfillim 15589  fmfnfmlem1 15594  fmfnfmlem2 15595  fmfnfmlem4 15597  fmfnfm 15598  flimfnfcls 15615  tailf 15633  filnetlem1 15640  filnetlem5 15644  filnet 15645  fzp1elp1 15794  fdc 15812  mettrifi 15847  lincmb01icc 15879  txsubsp 15912  txopn 15913  heiborlem14 15968  rrntotbnd 16022  lubun 16899  lubunNEW 16900  paddcom 17274  paddasslem11 17291  paddasslem12 17292  paddasslem13 17293  pmodlem1 17307  osumcllem6 17369  osumcllem9 17372  osumcllem11 17374  pexmidlem3 17380

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain