Theorem eqelssd 3968

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  ordtypelem9  9479  ordtypelem10  9480  oismo  9493  prlem934  10986  phimullem  16749  prmreclem5  16891  psssdm2  18540  sylow3lem3  19559  ablfacrp  19998  isdrng2  20652  fidomndrng  20682  imadrhmcl  20706  pjfo  21624  obs2ss  21638  frlmsslsp  21705  mplbas2  21949  restfpw  23066  2ndcsep  23346  ptclsg  23502  trfg  23778  restutopopn  24126  unirnblps  24307  unirnbl  24308  clsocv  25150  rrxbasefi  25310  pjth  25339  opnmbllem  25502  dvidlem  25816  dvaddf  25845  dvmulf  25846  dvcof  25852  dvcj  25854  dvrec  25859  dvcnv  25881  dvcnvre  25924  ftc1cn  25950  ulmdv  26312  pserdv  26339  ppisval2  27015  noseqrdgfn  28200  nbupgruvtxres  29334  ply1degltdimlem  33618  dimkerim  33623  fedgmul  33627  assafld  33633  reff  33829  dya2iocuni  34274  cvmsss2  35261  opnmbllem0  37650  ftc1cnnc  37686  lkrlsp  39095  cdleme50rnlem  40538  hdmaprnN  41858  hgmaprnN  41895  qsalrel  42228  kercvrlsm  43072  pwssplit4  43078  hbtlem5  43117  restuni3  45112  disjf1o  45185  unirnmapsn  45208  iunmapsn  45211  icoiccdif  45522  iccdificc  45537  lptioo2  45629  lptioo1  45630  qndenserrn  46297  intsaluni  46327  iundjiun  46458  meadjiunlem  46463  meaiininclem  46484  iunhoiioo  46674