Theorem eqelssd 3957

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

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

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 3920

This theorem is referenced by:  ordtypelem9  9418  ordtypelem10  9419  oismo  9432  prlem934  10927  phimullem  16690  prmreclem5  16832  psssdm2  18487  sylow3lem3  19508  ablfacrp  19947  isdrng2  20628  fidomndrng  20658  imadrhmcl  20682  pjfo  21622  obs2ss  21636  frlmsslsp  21703  mplbas2  21947  restfpw  23064  2ndcsep  23344  ptclsg  23500  trfg  23776  restutopopn  24124  unirnblps  24305  unirnbl  24306  clsocv  25148  rrxbasefi  25308  pjth  25337  opnmbllem  25500  dvidlem  25814  dvaddf  25843  dvmulf  25844  dvcof  25850  dvcj  25852  dvrec  25857  dvcnv  25879  dvcnvre  25922  ftc1cn  25948  ulmdv  26310  pserdv  26337  ppisval2  27013  noseqrdgfn  28205  nbupgruvtxres  29352  ply1degltdimlem  33595  dimkerim  33600  fedgmul  33604  assafld  33610  extdgfialg  33667  reff  33812  dya2iocuni  34257  cvmsss2  35257  opnmbllem0  37646  ftc1cnnc  37682  lkrlsp  39091  cdleme50rnlem  40533  hdmaprnN  41853  hgmaprnN  41890  qsalrel  42223  kercvrlsm  43066  pwssplit4  43072  hbtlem5  43111  restuni3  45106  disjf1o  45179  unirnmapsn  45202  iunmapsn  45205  icoiccdif  45515  iccdificc  45530  lptioo2  45622  lptioo1  45623  qndenserrn  46290  intsaluni  46320  iundjiun  46451  meadjiunlem  46456  meaiininclem  46477  iunhoiioo  46667