Theorem eqelssd 4017

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

Step	Hyp	Ref	Expression
1		eqelssd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		eqelssd.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
3	2	ex 412	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
4	3	ssrdv 4001	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
5	1, 4	eqssd 4013	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980

This theorem is referenced by:  wfrlem10OLD  8357  ordtypelem9  9564  ordtypelem10  9565  oismo  9578  prlem934  11071  phimullem  16813  prmreclem5  16954  psssdm2  18639  sylow3lem3  19662  ablfacrp  20101  isdrng2  20760  fidomndrng  20791  imadrhmcl  20815  pjfo  21753  obs2ss  21767  frlmsslsp  21834  mplbas2  22078  restfpw  23203  2ndcsep  23483  ptclsg  23639  trfg  23915  restutopopn  24263  unirnblps  24445  unirnbl  24446  clsocv  25298  rrxbasefi  25458  pjth  25487  opnmbllem  25650  dvidlem  25965  dvaddf  25994  dvmulf  25995  dvcof  26001  dvcj  26003  dvrec  26008  dvcnv  26030  dvcnvre  26073  ftc1cn  26099  ulmdv  26461  pserdv  26488  ppisval2  27163  noseqrdgfn  28327  nbupgruvtxres  29439  ply1degltdimlem  33650  dimkerim  33655  fedgmul  33659  assafld  33665  reff  33800  dya2iocuni  34265  cvmsss2  35259  opnmbllem0  37643  ftc1cnnc  37679  lkrlsp  39084  cdleme50rnlem  40527  hdmaprnN  41847  hgmaprnN  41884  qsalrel  42260  kercvrlsm  43072  pwssplit4  43078  hbtlem5  43117  restuni3  45058  disjf1o  45134  unirnmapsn  45157  iunmapsn  45160  icoiccdif  45477  iccdificc  45492  lptioo2  45587  lptioo1  45588  qndenserrn  46255  intsaluni  46285  iundjiun  46416  meadjiunlem  46421  meaiininclem  46442  iunhoiioo  46632