Theorem eqelssd 3951

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  ordtypelem9  9412  ordtypelem10  9413  oismo  9426  prlem934  10924  phimullem  16690  prmreclem5  16832  psssdm2  18487  sylow3lem3  19541  ablfacrp  19980  isdrng2  20658  fidomndrng  20688  imadrhmcl  20712  pjfo  21652  obs2ss  21666  frlmsslsp  21733  mplbas2  21977  restfpw  23094  2ndcsep  23374  ptclsg  23530  trfg  23806  restutopopn  24153  unirnblps  24334  unirnbl  24335  clsocv  25177  rrxbasefi  25337  pjth  25366  opnmbllem  25529  dvidlem  25843  dvaddf  25872  dvmulf  25873  dvcof  25879  dvcj  25881  dvrec  25886  dvcnv  25908  dvcnvre  25951  ftc1cn  25977  ulmdv  26339  pserdv  26366  ppisval2  27042  noseqrdgfn  28236  nbupgruvtxres  29385  ply1degltdimlem  33635  dimkerim  33640  fedgmul  33644  assafld  33650  extdgfialg  33707  reff  33852  dya2iocuni  34296  cvmsss2  35318  opnmbllem0  37706  ftc1cnnc  37742  lkrlsp  39211  cdleme50rnlem  40653  hdmaprnN  41973  hgmaprnN  42010  qsalrel  42343  kercvrlsm  43186  pwssplit4  43192  hbtlem5  43231  restuni3  45225  disjf1o  45298  unirnmapsn  45321  iunmapsn  45324  icoiccdif  45634  iccdificc  45649  lptioo2  45741  lptioo1  45742  qndenserrn  46407  intsaluni  46437  iundjiun  46568  meadjiunlem  46573  meaiininclem  46594  iunhoiioo  46784