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

Theorem eqelssd 4000
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 411 . . 3 (𝜑 → (𝑥𝐵𝑥𝐴))
43ssrdv 3984 . 2 (𝜑𝐵𝐴)
51, 4eqssd 3996 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  wcel 2099  wss 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ss 3963
This theorem is referenced by:  wfrlem10OLD  8340  ordtypelem9  9562  ordtypelem10  9563  oismo  9576  prlem934  11067  phimullem  16776  prmreclem5  16917  psssdm2  18601  sylow3lem3  19623  ablfacrp  20062  isdrng2  20717  fidomndrng  20748  imadrhmcl  20772  pjfo  21709  obs2ss  21723  frlmsslsp  21790  mplbas2  22045  restfpw  23171  2ndcsep  23451  ptclsg  23607  trfg  23883  restutopopn  24231  unirnblps  24413  unirnbl  24414  clsocv  25266  rrxbasefi  25426  pjth  25455  opnmbllem  25618  dvidlem  25932  dvaddf  25961  dvmulf  25962  dvcof  25968  dvcj  25970  dvrec  25975  dvcnv  25997  dvcnvre  26040  ftc1cn  26066  ulmdv  26429  pserdv  26456  ppisval2  27130  noseqrdgfn  28277  nbupgruvtxres  29340  ply1degltdimlem  33523  dimkerim  33528  fedgmul  33532  reff  33667  dya2iocuni  34130  cvmsss2  35115  opnmbllem0  37370  ftc1cnnc  37406  lkrlsp  38813  cdleme50rnlem  40256  hdmaprnN  41576  hgmaprnN  41613  qsalrel  41986  kercvrlsm  42781  pwssplit4  42787  hbtlem5  42826  restuni3  44756  disjf1o  44834  unirnmapsn  44857  iunmapsn  44860  icoiccdif  45178  iccdificc  45193  lptioo2  45288  lptioo1  45289  qndenserrn  45956  intsaluni  45986  iundjiun  46117  meadjiunlem  46122  meaiininclem  46143  iunhoiioo  46333
  Copyright terms: Public domain W3C validator