Theorem eqelssd 3913

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ⊆ wss 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875

This theorem is referenced by:  wfrlem10  7974  ordtypelem9  9023  ordtypelem10  9024  oismo  9037  prlem934  10493  phimullem  16171  prmreclem5  16311  psssdm2  17891  sylow3lem3  18821  ablfacrp  19256  isdrng2  19580  fidomndrng  20148  pjfo  20480  obs2ss  20494  frlmsslsp  20561  mplbas2  20802  restfpw  21879  2ndcsep  22159  ptclsg  22315  trfg  22591  restutopopn  22939  unirnblps  23121  unirnbl  23122  clsocv  23950  rrxbasefi  24110  pjth  24139  opnmbllem  24301  dvidlem  24614  dvaddf  24641  dvmulf  24642  dvcof  24647  dvcj  24649  dvrec  24654  dvcnv  24676  dvcnvre  24718  ftc1cn  24742  ulmdv  25097  pserdv  25123  ppisval2  25789  nbupgruvtxres  27296  dimkerim  31229  fedgmul  31233  reff  31310  dya2iocuni  31769  cvmsss2  32752  opnmbllem0  35373  ftc1cnnc  35409  lkrlsp  36678  cdleme50rnlem  38120  hdmaprnN  39440  hgmaprnN  39477  qsalrel  39721  kercvrlsm  40400  pwssplit4  40406  hbtlem5  40445  restuni3  42126  disjf1o  42188  unirnmapsn  42213  iunmapsn  42216  icoiccdif  42527  iccdificc  42542  lptioo2  42639  lptioo1  42640  qndenserrn  43307  intsaluni  43335  iundjiun  43465  meadjiunlem  43470  meaiininclem  43491  iunhoiioo  43681