Theorem eqelssd 3966

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 417	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
4	3	ssrdv 3951	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
5	1, 4	eqssd 3962	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  ordtypelem9  9488  ordtypelem10  9489  oismo  9502  prlem934  11018  phimullem  16838  prmreclem5  16980  psssdm2  18637  sylow3lem3  19699  ablfacrp  20138  isdrng2  20827  fidomndrng  20855  imadrhmcl  20878  pjfo  21834  obs2ss  21848  frlmsslsp  21915  mplbas2  22162  restfpw  23305  2ndcsep  23585  ptclsg  23741  trfg  24017  restutopopn  24364  unirnblps  24545  unirnbl  24546  clsocv  25378  rrxbasefi  25538  pjth  25567  opnmbllem  25729  dvidlem  26043  dvaddf  26070  dvmulf  26071  dvcof  26076  dvcj  26078  dvrec  26083  dvcnv  26105  dvcnvre  26147  ftc1cn  26171  ulmdv  26532  pserdv  26558  ppisval2  27235  noseqrdgfn  28465  nbupgruvtxres  29698  ply1degltdimlem  33957  dimkerim  33962  fedgmul  33966  assafld  33972  extdgfialg  34029  reff  34174  dya2iocuni  34618  cvmsss2  35699  opnmbllem0  38229  ftc1cnnc  38265  lkrlsp  39800  cdleme50rnlem  41242  hdmaprnN  42562  hgmaprnN  42599  qsalrel  42933  kercvrlsm  43736  pwssplit4  43742  hbtlem5  43781  restuni3  45762  disjf1o  45835  unirnmapsn  45856  iunmapsn  45859  icoiccdif  46166  iccdificc  46181  lptioo2  46273  lptioo1  46274  qndenserrn  46939  intsaluni  46969  iundjiun  47100  meadjiunlem  47105  meaiininclem  47126  iunhoiioo  47316