Theorem eqelssd 3988

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 415	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
4	3	ssrdv 3973	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
5	1, 4	eqssd 3984	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  wfrlem10  7964  ordtypelem9  8990  ordtypelem10  8991  oismo  9004  prlem934  10455  phimullem  16116  prmreclem5  16256  psssdm2  17825  sylow3lem3  18754  ablfacrp  19188  isdrng2  19512  fidomndrng  20080  mplbas2  20251  pjfo  20859  obs2ss  20873  frlmsslsp  20940  restfpw  21787  2ndcsep  22067  ptclsg  22223  trfg  22499  restutopopn  22847  unirnblps  23029  unirnbl  23030  clsocv  23853  rrxbasefi  24013  pjth  24042  opnmbllem  24202  dvidlem  24513  dvaddf  24539  dvmulf  24540  dvcof  24545  dvcj  24547  dvrec  24552  dvcnv  24574  dvcnvre  24616  ftc1cn  24640  ulmdv  24991  pserdv  25017  ppisval2  25682  nbupgruvtxres  27189  dimkerim  31023  fedgmul  31027  reff  31103  dya2iocuni  31541  cvmsss2  32521  opnmbllem0  34943  ftc1cnnc  34981  lkrlsp  36253  cdleme50rnlem  37695  hdmaprnN  39015  hgmaprnN  39052  qsalrel  39174  kercvrlsm  39732  pwssplit4  39738  hbtlem5  39777  restuni3  41433  disjf1o  41501  unirnmapsn  41526  iunmapsn  41529  icoiccdif  41849  iccdificc  41864  lptioo2  41961  lptioo1  41962  qndenserrn  42633  intsaluni  42661  iundjiun  42791  meadjiunlem  42796  meaiininclem  42817  iunhoiioo  43007