Theorem eqelssd 3965

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928

This theorem is referenced by:  ordtypelem9  9455  ordtypelem10  9456  oismo  9469  prlem934  10962  phimullem  16725  prmreclem5  16867  psssdm2  18522  sylow3lem3  19543  ablfacrp  19982  isdrng2  20663  fidomndrng  20693  imadrhmcl  20717  pjfo  21657  obs2ss  21671  frlmsslsp  21738  mplbas2  21982  restfpw  23099  2ndcsep  23379  ptclsg  23535  trfg  23811  restutopopn  24159  unirnblps  24340  unirnbl  24341  clsocv  25183  rrxbasefi  25343  pjth  25372  opnmbllem  25535  dvidlem  25849  dvaddf  25878  dvmulf  25879  dvcof  25885  dvcj  25887  dvrec  25892  dvcnv  25914  dvcnvre  25957  ftc1cn  25983  ulmdv  26345  pserdv  26372  ppisval2  27048  noseqrdgfn  28240  nbupgruvtxres  29387  ply1degltdimlem  33611  dimkerim  33616  fedgmul  33620  assafld  33626  reff  33822  dya2iocuni  34267  cvmsss2  35254  opnmbllem0  37643  ftc1cnnc  37679  lkrlsp  39088  cdleme50rnlem  40531  hdmaprnN  41851  hgmaprnN  41888  qsalrel  42221  kercvrlsm  43065  pwssplit4  43071  hbtlem5  43110  restuni3  45105  disjf1o  45178  unirnmapsn  45201  iunmapsn  45204  icoiccdif  45515  iccdificc  45530  lptioo2  45622  lptioo1  45623  qndenserrn  46290  intsaluni  46320  iundjiun  46451  meadjiunlem  46456  meaiininclem  46477  iunhoiioo  46667