Theorem eqelssd 3955

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  ordtypelem9  9433  ordtypelem10  9434  oismo  9447  prlem934  10946  phimullem  16708  prmreclem5  16850  psssdm2  18506  sylow3lem3  19560  ablfacrp  19999  isdrng2  20678  fidomndrng  20708  imadrhmcl  20732  pjfo  21672  obs2ss  21686  frlmsslsp  21753  mplbas2  21999  restfpw  23125  2ndcsep  23405  ptclsg  23561  trfg  23837  restutopopn  24184  unirnblps  24365  unirnbl  24366  clsocv  25208  rrxbasefi  25368  pjth  25397  opnmbllem  25560  dvidlem  25874  dvaddf  25903  dvmulf  25904  dvcof  25910  dvcj  25912  dvrec  25917  dvcnv  25939  dvcnvre  25982  ftc1cn  26008  ulmdv  26370  pserdv  26397  ppisval2  27073  noseqrdgfn  28304  nbupgruvtxres  29482  ply1degltdimlem  33781  dimkerim  33786  fedgmul  33790  assafld  33796  extdgfialg  33853  reff  33998  dya2iocuni  34442  cvmsss2  35470  opnmbllem0  37859  ftc1cnnc  37895  lkrlsp  39384  cdleme50rnlem  40826  hdmaprnN  42146  hgmaprnN  42183  qsalrel  42517  kercvrlsm  43346  pwssplit4  43352  hbtlem5  43391  restuni3  45383  disjf1o  45456  unirnmapsn  45479  iunmapsn  45482  icoiccdif  45791  iccdificc  45806  lptioo2  45898  lptioo1  45899  qndenserrn  46564  intsaluni  46594  iundjiun  46725  meadjiunlem  46730  meaiininclem  46751  iunhoiioo  46941