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

Theorem eqelssd 3963
Description: Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.)
Hypotheses
Ref Expression
eqelssd.1 (𝜑𝐴𝐵)
eqelssd.2 ((𝜑𝑥𝐵) → 𝑥𝐴)
Assertion
Ref Expression
eqelssd (𝜑𝐴 = 𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem eqelssd
StepHypRef Expression
1 eqelssd.1 . 2 (𝜑𝐴𝐵)
2 eqelssd.2 . . . 4 ((𝜑𝑥𝐵) → 𝑥𝐴)
32ex 413 . . 3 (𝜑 → (𝑥𝐵𝑥𝐴))
43ssrdv 3948 . 2 (𝜑𝐵𝐴)
51, 4eqssd 3959 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wss 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-in 3915  df-ss 3925
This theorem is referenced by:  wfrlem10OLD  8260  ordtypelem9  9458  ordtypelem10  9459  oismo  9472  prlem934  10965  phimullem  16643  prmreclem5  16784  psssdm2  18462  sylow3lem3  19402  ablfacrp  19836  isdrng2  20183  fidomndrng  20763  pjfo  21106  obs2ss  21120  frlmsslsp  21187  mplbas2  21427  restfpw  22514  2ndcsep  22794  ptclsg  22950  trfg  23226  restutopopn  23574  unirnblps  23756  unirnbl  23757  clsocv  24598  rrxbasefi  24758  pjth  24787  opnmbllem  24949  dvidlem  25263  dvaddf  25290  dvmulf  25291  dvcof  25296  dvcj  25298  dvrec  25303  dvcnv  25325  dvcnvre  25367  ftc1cn  25391  ulmdv  25746  pserdv  25772  ppisval2  26438  nbupgruvtxres  28241  dimkerim  32199  fedgmul  32203  reff  32289  dya2iocuni  32752  cvmsss2  33737  opnmbllem0  36081  ftc1cnnc  36117  lkrlsp  37531  cdleme50rnlem  38974  hdmaprnN  40294  hgmaprnN  40331  qsalrel  40629  kercvrlsm  41348  pwssplit4  41354  hbtlem5  41393  restuni3  43270  disjf1o  43346  unirnmapsn  43371  iunmapsn  43374  icoiccdif  43694  iccdificc  43709  lptioo2  43804  lptioo1  43805  qndenserrn  44472  intsaluni  44502  iundjiun  44633  meadjiunlem  44638  meaiininclem  44659  iunhoiioo  44849
  Copyright terms: Public domain W3C validator