Theorem eqelssd 3938

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  wfrlem10OLD  8120  ordtypelem9  9215  ordtypelem10  9216  oismo  9229  prlem934  10720  phimullem  16408  prmreclem5  16549  psssdm2  18214  sylow3lem3  19149  ablfacrp  19584  isdrng2  19916  fidomndrng  20492  pjfo  20832  obs2ss  20846  frlmsslsp  20913  mplbas2  21153  restfpw  22238  2ndcsep  22518  ptclsg  22674  trfg  22950  restutopopn  23298  unirnblps  23480  unirnbl  23481  clsocv  24319  rrxbasefi  24479  pjth  24508  opnmbllem  24670  dvidlem  24984  dvaddf  25011  dvmulf  25012  dvcof  25017  dvcj  25019  dvrec  25024  dvcnv  25046  dvcnvre  25088  ftc1cn  25112  ulmdv  25467  pserdv  25493  ppisval2  26159  nbupgruvtxres  27677  dimkerim  31610  fedgmul  31614  reff  31691  dya2iocuni  32150  cvmsss2  33136  opnmbllem0  35740  ftc1cnnc  35776  lkrlsp  37043  cdleme50rnlem  38485  hdmaprnN  39805  hgmaprnN  39842  qsalrel  40141  kercvrlsm  40824  pwssplit4  40830  hbtlem5  40869  restuni3  42556  disjf1o  42618  unirnmapsn  42643  iunmapsn  42646  icoiccdif  42952  iccdificc  42967  lptioo2  43062  lptioo1  43063  qndenserrn  43730  intsaluni  43758  iundjiun  43888  meadjiunlem  43893  meaiininclem  43914  iunhoiioo  44104