MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssel Structured version   Visualization version   GIF version

Theorem ssel 3803
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.
StepHypRef Expression
1 dfss2 3797 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 207 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 2225 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 601 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 2008 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2813 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2813 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 287 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1635   = wceq 1637  wex 1859  wcel 2157  wss 3780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-in 3787  df-ss 3794
This theorem is referenced by:  ssel2  3804  sseli  3805  sseld  3808  sstr2  3816  nelss  3872  ssrexf  3873  ssralv  3874  ssrexv  3875  ralss  3876  rexss  3877  ssconb  3953  sscon  3954  ssdif  3955  unss1  3992  ssrin  4045  difin2  4102  reuss2  4119  reupick  4123  elpwunsn  4428  sssn  4558  uniss  4664  ss2iun  4739  ssiun  4765  iinss  4774  disjss2  4826  disjss1  4829  pwnss  5035  sspwb  5120  ssopab2b  5210  pwssun  5228  soss  5263  xpss12  5339  frinxp  5400  ssrel  5423  ssrelOLD  5424  ssrel2  5426  ssrelrel  5436  dmss  5538  elreldm  5565  dmcosseq  5602  relssres  5655  iss  5666  resopab2  5667  idrefOLD  5734  ssrnres  5797  dfco2a  5863  cores  5866  oneqmini  6002  sucssel  6043  onssneli  6060  onssnel2i  6061  funssres  6154  fununi  6185  dfimafn  6476  funimass4  6478  funimass3  6565  dff3  6604  dff4  6605  funfvima2  6728  funfvima3  6730  f1elima  6754  isomin  6821  isofrlem  6824  riotass2  6872  ssoprab2b  6952  resoprab2  6997  ssorduni  7225  onint  7235  oninton  7240  ssnlim  7323  releldm2  7460  reldmtpos  7605  dmtpos  7609  wfrlem10  7670  onfununi  7684  tz7.48lem  7782  tz7.49  7786  omeulem1  7909  omeulem2  7910  omsmolem  7980  omsmo  7981  ss2ixp  8168  boxriin  8197  onomeneq  8399  unblem1  8461  unblem3  8463  fiint  8486  inf3lem2  8783  cantnflem2  8844  tcel  8878  tz9.13  8911  rankr1ag  8922  rankpwi  8943  rankelb  8944  bndrank  8961  cardlim  9091  carduni  9100  acni2  9162  dfac12r  9263  cfub  9366  cflim2  9380  fin1a2lem9  9525  axdc3lem2  9568  axdclem2  9637  gch2  9792  eltsk2g  9868  suplem1pr  10169  negn0  10754  negf1o  10755  fimaxre  11263  negfi  11266  fiminre  11267  lbreu  11268  lbinf  11271  sup2  11274  sup3  11275  infm3  11277  infregelb  11302  uzwo  11990  eqreznegel  12013  xrsupsslem  12375  xrinfmsslem  12376  supxrpnf  12386  supxrunb1  12387  supxrunb2  12388  iccsupr  12505  ssnn0fi  13028  incexclem  14810  fprodmodd  14968  sumeven  15350  sumodd  15351  gcdcllem1  15460  lcmfnnval  15576  lcmfnncl  15581  dvdslcmf  15583  lcmfunsnlem2lem2  15591  lcmfdvdsb  15595  lubel  17347  clatleglb  17351  mulgpropd  17806  sylow2a  18255  efgi2  18359  lspsnel6  19221  submabas  20616  pmatcollpw3lem  20822  elcls2  21113  isclo2  21127  cmpsublem  21437  cmpsub  21438  hauscmplem  21444  1stcelcls  21499  llyss  21517  nllyss  21518  txkgen  21690  nrmr0reg  21787  uffix  21959  ufinffr  21967  ufilen  21968  fmfnfmlem2  21993  alexsubALTlem2  22086  alexsubALT  22089  metrest  22563  iccntr  22858  reconnlem2  22864  clmneg1  23115  clmvscom  23123  caubl  23340  ulmss  24388  axcontlem4  26084  ocsh  28493  ococss  28503  shorth  28505  spansnss2  28785  h1datomi  28791  pjss2i  28890  pjssmii  28891  pjorthcoi  29379  pj3si  29417  ssrelf  29775  dfimafnf  29786  funimass4f  29787  mptssALT  29824  1stpreima  29834  2ndpreima  29835  ordtconnlem1  30318  indpi1  30430  bnj518  31301  cvmlift2lem1  31629  dfon2lem6  32035  trpredmintr  32073  orderseqlem  32095  frrlem5b  32128  frrlem5d  32130  nofv  32153  nocvxminlem  32236  nocvxmin  32237  limsucncmpi  32783  finxpreclem4  33566  poimirlem3  33744  poimirlem29  33770  poimirlem32  33773  ismtyres  33937  ispridlc  34199  iss2  34444  paddss1  35616  paddss2  35617  lspindp5  37569  pw2f1ocnv  38123  ss2iundf  38469  iunrelexp0  38512  gneispace0nelrn3  38958  nzss  39034  onfrALTlem3  39275  onfrALTlem2  39277  sspwtr  39563  sspwtrALT  39564  sspwtrALT2  39570  pwtrVD  39571  pwtrrVD  39572  suctrALT2VD  39583  suctrALT2  39584  onfrALTlem3VD  39635  onfrALTlem2VD  39637  iinssf  39836  qndenserrnopnlem  41014  dfaimafn  41772  sprsymrelfolem2  42329  mgmplusfreseq  42359  gsumlsscl  42750  lincfsuppcl  42788  linccl  42789  onsetrec  43040
  Copyright terms: Public domain W3C validator