Theorem eqelssd 3980

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943

This theorem is referenced by:  wfrlem10OLD  8332  ordtypelem9  9540  ordtypelem10  9541  oismo  9554  prlem934  11047  phimullem  16798  prmreclem5  16940  psssdm2  18591  sylow3lem3  19610  ablfacrp  20049  isdrng2  20703  fidomndrng  20733  imadrhmcl  20757  pjfo  21675  obs2ss  21689  frlmsslsp  21756  mplbas2  22000  restfpw  23117  2ndcsep  23397  ptclsg  23553  trfg  23829  restutopopn  24177  unirnblps  24358  unirnbl  24359  clsocv  25202  rrxbasefi  25362  pjth  25391  opnmbllem  25554  dvidlem  25868  dvaddf  25897  dvmulf  25898  dvcof  25904  dvcj  25906  dvrec  25911  dvcnv  25933  dvcnvre  25976  ftc1cn  26002  ulmdv  26364  pserdv  26391  ppisval2  27067  noseqrdgfn  28252  nbupgruvtxres  29386  ply1degltdimlem  33662  dimkerim  33667  fedgmul  33671  assafld  33677  reff  33870  dya2iocuni  34315  cvmsss2  35296  opnmbllem0  37680  ftc1cnnc  37716  lkrlsp  39120  cdleme50rnlem  40563  hdmaprnN  41883  hgmaprnN  41920  qsalrel  42291  kercvrlsm  43107  pwssplit4  43113  hbtlem5  43152  restuni3  45142  disjf1o  45215  unirnmapsn  45238  iunmapsn  45241  icoiccdif  45553  iccdificc  45568  lptioo2  45660  lptioo1  45661  qndenserrn  46328  intsaluni  46358  iundjiun  46489  meadjiunlem  46494  meaiininclem  46515  iunhoiioo  46705