Theorem eqelssd 3968

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  wfrlem10OLD  8269  ordtypelem9  9471  ordtypelem10  9472  oismo  9485  prlem934  10978  phimullem  16662  prmreclem5  16803  psssdm2  18484  sylow3lem3  19425  ablfacrp  19859  isdrng2  20238  imadrhmcl  20320  fidomndrng  20815  pjfo  21158  obs2ss  21172  frlmsslsp  21239  mplbas2  21480  restfpw  22567  2ndcsep  22847  ptclsg  23003  trfg  23279  restutopopn  23627  unirnblps  23809  unirnbl  23810  clsocv  24651  rrxbasefi  24811  pjth  24840  opnmbllem  25002  dvidlem  25316  dvaddf  25343  dvmulf  25344  dvcof  25349  dvcj  25351  dvrec  25356  dvcnv  25378  dvcnvre  25420  ftc1cn  25444  ulmdv  25799  pserdv  25825  ppisval2  26491  nbupgruvtxres  28418  ply1degltdimlem  32404  dimkerim  32409  fedgmul  32413  reff  32509  dya2iocuni  32972  cvmsss2  33955  opnmbllem0  36187  ftc1cnnc  36223  lkrlsp  37637  cdleme50rnlem  39080  hdmaprnN  40400  hgmaprnN  40437  qsalrel  40735  kercvrlsm  41468  pwssplit4  41474  hbtlem5  41513  restuni3  43450  disjf1o  43532  unirnmapsn  43556  iunmapsn  43559  icoiccdif  43882  iccdificc  43897  lptioo2  43992  lptioo1  43993  qndenserrn  44660  intsaluni  44690  iundjiun  44821  meadjiunlem  44826  meaiininclem  44847  iunhoiioo  45037