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

Theorem eqelssd 4005
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 412 . . 3 (𝜑 → (𝑥𝐵𝑥𝐴))
43ssrdv 3989 . 2 (𝜑𝐵𝐴)
51, 4eqssd 4001 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968
This theorem is referenced by:  wfrlem10OLD  8358  ordtypelem9  9566  ordtypelem10  9567  oismo  9580  prlem934  11073  phimullem  16816  prmreclem5  16958  psssdm2  18626  sylow3lem3  19647  ablfacrp  20086  isdrng2  20743  fidomndrng  20774  imadrhmcl  20798  pjfo  21735  obs2ss  21749  frlmsslsp  21816  mplbas2  22060  restfpw  23187  2ndcsep  23467  ptclsg  23623  trfg  23899  restutopopn  24247  unirnblps  24429  unirnbl  24430  clsocv  25284  rrxbasefi  25444  pjth  25473  opnmbllem  25636  dvidlem  25950  dvaddf  25979  dvmulf  25980  dvcof  25986  dvcj  25988  dvrec  25993  dvcnv  26015  dvcnvre  26058  ftc1cn  26084  ulmdv  26446  pserdv  26473  ppisval2  27148  noseqrdgfn  28312  nbupgruvtxres  29424  ply1degltdimlem  33673  dimkerim  33678  fedgmul  33682  assafld  33688  reff  33838  dya2iocuni  34285  cvmsss2  35279  opnmbllem0  37663  ftc1cnnc  37699  lkrlsp  39103  cdleme50rnlem  40546  hdmaprnN  41866  hgmaprnN  41903  qsalrel  42281  kercvrlsm  43095  pwssplit4  43101  hbtlem5  43140  restuni3  45123  disjf1o  45196  unirnmapsn  45219  iunmapsn  45222  icoiccdif  45537  iccdificc  45552  lptioo2  45646  lptioo1  45647  qndenserrn  46314  intsaluni  46344  iundjiun  46475  meadjiunlem  46480  meaiininclem  46501  iunhoiioo  46691
  Copyright terms: Public domain W3C validator