Theorem eqelssd 3971

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

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

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 2702

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

This theorem is referenced by:  ordtypelem9  9486  ordtypelem10  9487  oismo  9500  prlem934  10993  phimullem  16756  prmreclem5  16898  psssdm2  18547  sylow3lem3  19566  ablfacrp  20005  isdrng2  20659  fidomndrng  20689  imadrhmcl  20713  pjfo  21631  obs2ss  21645  frlmsslsp  21712  mplbas2  21956  restfpw  23073  2ndcsep  23353  ptclsg  23509  trfg  23785  restutopopn  24133  unirnblps  24314  unirnbl  24315  clsocv  25157  rrxbasefi  25317  pjth  25346  opnmbllem  25509  dvidlem  25823  dvaddf  25852  dvmulf  25853  dvcof  25859  dvcj  25861  dvrec  25866  dvcnv  25888  dvcnvre  25931  ftc1cn  25957  ulmdv  26319  pserdv  26346  ppisval2  27022  noseqrdgfn  28207  nbupgruvtxres  29341  ply1degltdimlem  33625  dimkerim  33630  fedgmul  33634  assafld  33640  reff  33836  dya2iocuni  34281  cvmsss2  35268  opnmbllem0  37657  ftc1cnnc  37693  lkrlsp  39102  cdleme50rnlem  40545  hdmaprnN  41865  hgmaprnN  41902  qsalrel  42235  kercvrlsm  43079  pwssplit4  43085  hbtlem5  43124  restuni3  45119  disjf1o  45192  unirnmapsn  45215  iunmapsn  45218  icoiccdif  45529  iccdificc  45544  lptioo2  45636  lptioo1  45637  qndenserrn  46304  intsaluni  46334  iundjiun  46465  meadjiunlem  46470  meaiininclem  46491  iunhoiioo  46681