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 1542   ∈ wcel 2114   ⊆ wss 3903

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 3920

This theorem is referenced by:  ordtypelem9  9443  ordtypelem10  9444  oismo  9457  prlem934  10956  phimullem  16718  prmreclem5  16860  psssdm2  18516  sylow3lem3  19573  ablfacrp  20012  isdrng2  20691  fidomndrng  20721  imadrhmcl  20745  pjfo  21685  obs2ss  21699  frlmsslsp  21766  mplbas2  22012  restfpw  23138  2ndcsep  23418  ptclsg  23574  trfg  23850  restutopopn  24197  unirnblps  24378  unirnbl  24379  clsocv  25221  rrxbasefi  25381  pjth  25410  opnmbllem  25573  dvidlem  25887  dvaddf  25916  dvmulf  25917  dvcof  25923  dvcj  25925  dvrec  25930  dvcnv  25952  dvcnvre  25995  ftc1cn  26021  ulmdv  26383  pserdv  26410  ppisval2  27086  noseqrdgfn  28317  nbupgruvtxres  29496  ply1degltdimlem  33804  dimkerim  33809  fedgmul  33813  assafld  33819  extdgfialg  33876  reff  34021  dya2iocuni  34465  cvmsss2  35494  opnmbllem0  37911  ftc1cnnc  37947  lkrlsp  39482  cdleme50rnlem  40924  hdmaprnN  42244  hgmaprnN  42281  qsalrel  42615  kercvrlsm  43444  pwssplit4  43450  hbtlem5  43489  restuni3  45481  disjf1o  45554  unirnmapsn  45576  iunmapsn  45579  icoiccdif  45888  iccdificc  45903  lptioo2  45995  lptioo1  45996  qndenserrn  46661  intsaluni  46691  iundjiun  46822  meadjiunlem  46827  meaiininclem  46848  iunhoiioo  47038