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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1561   ∈ wcel 2143   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-ss 3922

This theorem is referenced by:  ordtypelem9  9475  ordtypelem10  9476  oismo  9489  prlem934  10992  phimullem  16815  prmreclem5  16957  psssdm2  18614  sylow3lem3  19670  ablfacrp  20109  isdrng2  20794  fidomndrng  20824  imadrhmcl  20847  pjfo  21768  obs2ss  21782  frlmsslsp  21849  mplbas2  22096  restfpw  23240  2ndcsep  23520  ptclsg  23676  trfg  23952  restutopopn  24299  unirnblps  24480  unirnbl  24481  clsocv  25313  rrxbasefi  25473  pjth  25502  opnmbllem  25664  dvidlem  25978  dvaddf  26005  dvmulf  26006  dvcof  26011  dvcj  26013  dvrec  26018  dvcnv  26040  dvcnvre  26082  ftc1cn  26106  ulmdv  26467  pserdv  26493  ppisval2  27170  noseqrdgfn  28400  nbupgruvtxres  29609  ply1degltdimlem  33920  dimkerim  33925  fedgmul  33929  assafld  33935  extdgfialg  33992  reff  34137  dya2iocuni  34581  cvmsss2  35625  opnmbllem0  38156  ftc1cnnc  38192  lkrlsp  39727  cdleme50rnlem  41169  hdmaprnN  42489  hgmaprnN  42526  qsalrel  42858  kercvrlsm  43661  pwssplit4  43667  hbtlem5  43706  restuni3  45697  disjf1o  45770  unirnmapsn  45791  iunmapsn  45794  icoiccdif  46101  iccdificc  46116  lptioo2  46208  lptioo1  46209  qndenserrn  46874  intsaluni  46904  iundjiun  47035  meadjiunlem  47040  meaiininclem  47061  iunhoiioo  47251