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

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

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