Theorem eqelssd 3959

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  ordtypelem9  9496  ordtypelem10  9497  oismo  9510  prlem934  11038  phimullem  16865  prmreclem5  17007  psssdm2  18664  sylow3lem3  19748  ablfacrp  20187  isdrng2  20898  fidomndrng  20932  imadrhmcl  20955  pjfo  21920  obs2ss  21934  frlmsslsp  22001  mplbas2  22248  restfpw  23391  2ndcsep  23672  ptclsg  23828  trfg  24104  restutopopn  24451  unirnblps  24632  unirnbl  24633  clsocv  25465  rrxbasefi  25625  pjth  25654  opnmbllem  25816  dvidlem  26130  dvaddf  26157  dvmulf  26158  dvcof  26163  dvcj  26165  dvrec  26170  dvcnv  26192  dvcnvre  26234  ftc1cn  26258  ulmdv  26622  pserdv  26648  ppisval2  27325  noseqrdgfn  28555  nbupgruvtxres  29820  ply1degltdimlem  34081  dimkerim  34086  fedgmul  34090  assafld  34096  extdgfialg  34153  reff  34298  dya2iocuni  34743  cvmsss2  35808  opnmbllem0  38369  ftc1cnnc  38405  lkrlsp  39939  cdleme50rnlem  41381  hdmaprnN  42701  hgmaprnN  42738  qsalrel  43072  kercvrlsm  43888  pwssplit4  43894  hbtlem5  43933  restuni3  45914  disjf1o  45987  unirnmapsn  46008  iunmapsn  46011  icoiccdif  46318  iccdificc  46333  lptioo2  46425  lptioo1  46426  qndenserrn  47091  intsaluni  47121  iundjiun  47252  meadjiunlem  47257  meaiininclem  47278  iunhoiioo  47468