Theorem eqelssd 3944

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 3928	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
5	1, 4	eqssd 3940	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  ordtypelem9  9436  ordtypelem10  9437  oismo  9450  prlem934  10951  phimullem  16744  prmreclem5  16886  psssdm2  18542  sylow3lem3  19599  ablfacrp  20038  isdrng2  20715  fidomndrng  20745  imadrhmcl  20769  pjfo  21709  obs2ss  21723  frlmsslsp  21790  mplbas2  22034  restfpw  23158  2ndcsep  23438  ptclsg  23594  trfg  23870  restutopopn  24217  unirnblps  24398  unirnbl  24399  clsocv  25231  rrxbasefi  25391  pjth  25420  opnmbllem  25582  dvidlem  25896  dvaddf  25923  dvmulf  25924  dvcof  25929  dvcj  25931  dvrec  25936  dvcnv  25958  dvcnvre  26000  ftc1cn  26024  ulmdv  26385  pserdv  26411  ppisval2  27086  noseqrdgfn  28316  nbupgruvtxres  29494  ply1degltdimlem  33786  dimkerim  33791  fedgmul  33795  assafld  33801  extdgfialg  33858  reff  34003  dya2iocuni  34447  cvmsss2  35476  opnmbllem0  37995  ftc1cnnc  38031  lkrlsp  39566  cdleme50rnlem  41008  hdmaprnN  42328  hgmaprnN  42365  qsalrel  42698  kercvrlsm  43533  pwssplit4  43539  hbtlem5  43578  restuni3  45570  disjf1o  45643  unirnmapsn  45665  iunmapsn  45668  icoiccdif  45976  iccdificc  45991  lptioo2  46083  lptioo1  46084  qndenserrn  46749  intsaluni  46779  iundjiun  46910  meadjiunlem  46915  meaiininclem  46936  iunhoiioo  47126