Theorem eqelssd 4005

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

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

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 2708

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

This theorem is referenced by:  wfrlem10OLD  8358  ordtypelem9  9566  ordtypelem10  9567  oismo  9580  prlem934  11073  phimullem  16816  prmreclem5  16958  psssdm2  18626  sylow3lem3  19647  ablfacrp  20086  isdrng2  20743  fidomndrng  20774  imadrhmcl  20798  pjfo  21735  obs2ss  21749  frlmsslsp  21816  mplbas2  22060  restfpw  23187  2ndcsep  23467  ptclsg  23623  trfg  23899  restutopopn  24247  unirnblps  24429  unirnbl  24430  clsocv  25284  rrxbasefi  25444  pjth  25473  opnmbllem  25636  dvidlem  25950  dvaddf  25979  dvmulf  25980  dvcof  25986  dvcj  25988  dvrec  25993  dvcnv  26015  dvcnvre  26058  ftc1cn  26084  ulmdv  26446  pserdv  26473  ppisval2  27148  noseqrdgfn  28312  nbupgruvtxres  29424  ply1degltdimlem  33673  dimkerim  33678  fedgmul  33682  assafld  33688  reff  33838  dya2iocuni  34285  cvmsss2  35279  opnmbllem0  37663  ftc1cnnc  37699  lkrlsp  39103  cdleme50rnlem  40546  hdmaprnN  41866  hgmaprnN  41903  qsalrel  42281  kercvrlsm  43095  pwssplit4  43101  hbtlem5  43140  restuni3  45123  disjf1o  45196  unirnmapsn  45219  iunmapsn  45222  icoiccdif  45537  iccdificc  45552  lptioo2  45646  lptioo1  45647  qndenserrn  46314  intsaluni  46344  iundjiun  46475  meadjiunlem  46480  meaiininclem  46501  iunhoiioo  46691