Theorem eqelssd 4030

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  wfrlem10OLD  8374  ordtypelem9  9595  ordtypelem10  9596  oismo  9609  prlem934  11102  phimullem  16826  prmreclem5  16967  psssdm2  18651  sylow3lem3  19671  ablfacrp  20110  isdrng2  20765  fidomndrng  20796  imadrhmcl  20820  pjfo  21758  obs2ss  21772  frlmsslsp  21839  mplbas2  22083  restfpw  23208  2ndcsep  23488  ptclsg  23644  trfg  23920  restutopopn  24268  unirnblps  24450  unirnbl  24451  clsocv  25303  rrxbasefi  25463  pjth  25492  opnmbllem  25655  dvidlem  25970  dvaddf  25999  dvmulf  26000  dvcof  26006  dvcj  26008  dvrec  26013  dvcnv  26035  dvcnvre  26078  ftc1cn  26104  ulmdv  26464  pserdv  26491  ppisval2  27166  noseqrdgfn  28330  nbupgruvtxres  29442  ply1degltdimlem  33635  dimkerim  33640  fedgmul  33644  assafld  33650  reff  33785  dya2iocuni  34248  cvmsss2  35242  opnmbllem0  37616  ftc1cnnc  37652  lkrlsp  39058  cdleme50rnlem  40501  hdmaprnN  41821  hgmaprnN  41858  qsalrel  42235  kercvrlsm  43040  pwssplit4  43046  hbtlem5  43085  restuni3  45020  disjf1o  45098  unirnmapsn  45121  iunmapsn  45124  icoiccdif  45442  iccdificc  45457  lptioo2  45552  lptioo1  45553  qndenserrn  46220  intsaluni  46250  iundjiun  46381  meadjiunlem  46386  meaiininclem  46407  iunhoiioo  46597