Theorem eqelssd 3929

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  ordtypelem9  9520  ordtypelem10  9521  oismo  9534  prlem934  11118  phimullem  16956  prmreclem5  17098  psssdm2  18755  sylow3lem3  19843  ablfacrp  20282  isdrng2  20997  fidomndrng  21031  imadrhmcl  21054  pjfo  22021  obs2ss  22035  frlmsslsp  22102  mplbas2  22351  restfpw  23497  2ndcsep  23778  ptclsg  23934  trfg  24210  restutopopn  24557  unirnblps  24738  unirnbl  24739  clsocv  25571  rrxbasefi  25731  pjth  25760  opnmbllem  25922  dvidlem  26235  dvaddf  26262  dvmulf  26263  dvcof  26268  dvcj  26270  dvrec  26275  dvcnv  26297  dvcnvre  26339  ftc1cn  26363  ulmdv  26730  pserdv  26756  ppisval2  27432  noseqrdgfn  28692  nbupgruvtxres  29988  ply1degltdimlem  34254  dimkerim  34259  fedgmul  34263  assafld  34269  extdgfialg  34326  reff  34471  dya2iocuni  34915  cvmsss2  36039  opnmbllem0  38575  ftc1cnnc  38611  lkrlsp  40160  cdleme50rnlem  41602  hdmaprnN  42922  hgmaprnN  42959  qsalrel  43293  kercvrlsm  44085  pwssplit4  44091  hbtlem5  44130  restuni3  46133  disjf1o  46206  unirnmapsn  46227  iunmapsn  46230  icoiccdif  46536  iccdificc  46551  lptioo2  46643  lptioo1  46644  qndenserrn  47309  intsaluni  47339  iundjiun  47470  meadjiunlem  47475  meaiininclem  47496  iunhoiioo  47686  tmachlem-exlargecover  47954