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

Theorem eqelssd 3970
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 414 . . 3 (𝜑 → (𝑥𝐵𝑥𝐴))
43ssrdv 3955 . 2 (𝜑𝐵𝐴)
51, 4eqssd 3966 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  wfrlem10OLD  8269  ordtypelem9  9469  ordtypelem10  9470  oismo  9483  prlem934  10976  phimullem  16658  prmreclem5  16799  psssdm2  18477  sylow3lem3  19418  ablfacrp  19852  isdrng2  20212  fidomndrng  20794  pjfo  21137  obs2ss  21151  frlmsslsp  21218  mplbas2  21459  restfpw  22546  2ndcsep  22826  ptclsg  22982  trfg  23258  restutopopn  23606  unirnblps  23788  unirnbl  23789  clsocv  24630  rrxbasefi  24790  pjth  24819  opnmbllem  24981  dvidlem  25295  dvaddf  25322  dvmulf  25323  dvcof  25328  dvcj  25330  dvrec  25335  dvcnv  25357  dvcnvre  25399  ftc1cn  25423  ulmdv  25778  pserdv  25804  ppisval2  26470  nbupgruvtxres  28397  dimkerim  32362  fedgmul  32366  reff  32460  dya2iocuni  32923  cvmsss2  33908  opnmbllem0  36143  ftc1cnnc  36179  lkrlsp  37593  cdleme50rnlem  39036  hdmaprnN  40356  hgmaprnN  40393  qsalrel  40693  imadrhmcl  40745  kercvrlsm  41439  pwssplit4  41445  hbtlem5  41484  restuni3  43402  disjf1o  43484  unirnmapsn  43509  iunmapsn  43512  icoiccdif  43836  iccdificc  43851  lptioo2  43946  lptioo1  43947  qndenserrn  44614  intsaluni  44644  iundjiun  44775  meadjiunlem  44780  meaiininclem  44801  iunhoiioo  44991
  Copyright terms: Public domain W3C validator