Theorem eqelssd 3953

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916

This theorem is referenced by:  ordtypelem9  9429  ordtypelem10  9430  oismo  9443  prlem934  10942  phimullem  16704  prmreclem5  16846  psssdm2  18502  sylow3lem3  19556  ablfacrp  19995  isdrng2  20674  fidomndrng  20704  imadrhmcl  20728  pjfo  21668  obs2ss  21682  frlmsslsp  21749  mplbas2  21995  restfpw  23121  2ndcsep  23401  ptclsg  23557  trfg  23833  restutopopn  24180  unirnblps  24361  unirnbl  24362  clsocv  25204  rrxbasefi  25364  pjth  25393  opnmbllem  25556  dvidlem  25870  dvaddf  25899  dvmulf  25900  dvcof  25906  dvcj  25908  dvrec  25913  dvcnv  25935  dvcnvre  25978  ftc1cn  26004  ulmdv  26366  pserdv  26393  ppisval2  27069  noseqrdgfn  28267  nbupgruvtxres  29429  ply1degltdimlem  33728  dimkerim  33733  fedgmul  33737  assafld  33743  extdgfialg  33800  reff  33945  dya2iocuni  34389  cvmsss2  35417  opnmbllem0  37796  ftc1cnnc  37832  lkrlsp  39301  cdleme50rnlem  40743  hdmaprnN  42063  hgmaprnN  42100  qsalrel  42438  kercvrlsm  43267  pwssplit4  43273  hbtlem5  43312  restuni3  45304  disjf1o  45377  unirnmapsn  45400  iunmapsn  45403  icoiccdif  45712  iccdificc  45727  lptioo2  45819  lptioo1  45820  qndenserrn  46485  intsaluni  46515  iundjiun  46646  meadjiunlem  46651  meaiininclem  46672  iunhoiioo  46862