Theorem eqelssd 3936

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  ordtypelem9  9432  ordtypelem10  9433  oismo  9446  prlem934  10948  phimullem  16741  prmreclem5  16883  psssdm2  18539  sylow3lem3  19596  ablfacrp  20035  isdrng2  20716  fidomndrng  20746  imadrhmcl  20770  pjfo  21691  obs2ss  21705  frlmsslsp  21772  mplbas2  22019  restfpw  23163  2ndcsep  23443  ptclsg  23599  trfg  23875  restutopopn  24222  unirnblps  24403  unirnbl  24404  clsocv  25236  rrxbasefi  25396  pjth  25425  opnmbllem  25587  dvidlem  25901  dvaddf  25928  dvmulf  25929  dvcof  25934  dvcj  25936  dvrec  25941  dvcnv  25963  dvcnvre  26005  ftc1cn  26029  ulmdv  26387  pserdv  26413  ppisval2  27087  noseqrdgfn  28317  nbupgruvtxres  29495  ply1degltdimlem  33815  dimkerim  33820  fedgmul  33824  assafld  33830  extdgfialg  33887  reff  34032  dya2iocuni  34476  cvmsss2  35511  opnmbllem0  38032  ftc1cnnc  38068  lkrlsp  39603  cdleme50rnlem  41045  hdmaprnN  42365  hgmaprnN  42402  qsalrel  42734  kercvrlsm  43537  pwssplit4  43543  hbtlem5  43582  restuni3  45573  disjf1o  45646  unirnmapsn  45667  iunmapsn  45670  icoiccdif  45977  iccdificc  45992  lptioo2  46084  lptioo1  46085  qndenserrn  46750  intsaluni  46780  iundjiun  46911  meadjiunlem  46916  meaiininclem  46937  iunhoiioo  47127