Theorem eqelssd 3952

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 418	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
4	3	ssrdv 3937	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
5	1, 4	eqssd 3948	1 ⊢ (𝜑 → 𝐴 = 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  ordtypelem9  9505  ordtypelem10  9506  oismo  9519  prlem934  11067  phimullem  16895  prmreclem5  17037  psssdm2  18694  sylow3lem3  19782  ablfacrp  20221  isdrng2  20936  fidomndrng  20970  imadrhmcl  20993  pjfo  21960  obs2ss  21974  frlmsslsp  22041  mplbas2  22290  restfpw  23436  2ndcsep  23717  ptclsg  23873  trfg  24149  restutopopn  24496  unirnblps  24677  unirnbl  24678  clsocv  25510  rrxbasefi  25670  pjth  25699  opnmbllem  25861  dvidlem  26174  dvaddf  26201  dvmulf  26202  dvcof  26207  dvcj  26209  dvrec  26214  dvcnv  26236  dvcnvre  26278  ftc1cn  26302  ulmdv  26671  pserdv  26697  ppisval2  27373  noseqrdgfn  28603  nbupgruvtxres  29899  ply1degltdimlem  34165  dimkerim  34170  fedgmul  34174  assafld  34180  extdgfialg  34237  reff  34382  dya2iocuni  34827  cvmsss2  35936  opnmbllem0  38470  ftc1cnnc  38506  lkrlsp  40040  cdleme50rnlem  41482  hdmaprnN  42802  hgmaprnN  42839  qsalrel  43173  kercvrlsm  43989  pwssplit4  43995  hbtlem5  44034  restuni3  46015  disjf1o  46088  unirnmapsn  46109  iunmapsn  46112  icoiccdif  46419  iccdificc  46434  lptioo2  46526  lptioo1  46527  qndenserrn  47192  intsaluni  47222  iundjiun  47353  meadjiunlem  47358  meaiininclem  47379  iunhoiioo  47569  tmachlem-exlargecover  47837