Theorem eqelssd 3958

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ⊆ wss 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is used by:  ordtypelem9  9484  ordtypelem10  9485  oismo  9498  prlem934  11022  phimullem  16842  prmreclem5  16984  psssdm2  18641  sylow3lem3  19703  ablfacrp  20142  isdrng2  20852  fidomndrng  20886  imadrhmcl  20909  pjfo  21874  obs2ss  21888  frlmsslsp  21955  mplbas2  22202  restfpw  23345  2ndcsep  23625  ptclsg  23781  trfg  24057  restutopopn  24404  unirnblps  24585  unirnbl  24586  clsocv  25418  rrxbasefi  25578  pjth  25607  opnmbllem  25769  dvidlem  26083  dvaddf  26110  dvmulf  26111  dvcof  26116  dvcj  26118  dvrec  26123  dvcnv  26145  dvcnvre  26187  ftc1cn  26211  ulmdv  26575  pserdv  26601  ppisval2  27278  noseqrdgfn  28508  nbupgruvtxres  29766  ply1degltdimlem  34021  dimkerim  34026  fedgmul  34030  assafld  34036  extdgfialg  34093  reff  34238  dya2iocuni  34682  cvmsss2  35774  opnmbllem0  38335  ftc1cnnc  38371  lkrlsp  39904  cdleme50rnlem  41346  hdmaprnN  42666  hgmaprnN  42703  qsalrel  43037  kercvrlsm  43838  pwssplit4  43844  hbtlem5  43883  restuni3  45864  disjf1o  45937  unirnmapsn  45958  iunmapsn  45961  icoiccdif  46268  iccdificc  46283  lptioo2  46375  lptioo1  46376  qndenserrn  47041  intsaluni  47071  iundjiun  47202  meadjiunlem  47207  meaiininclem  47228  iunhoiioo  47418