Theorem eqelssd 3943

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  ordtypelem9  9441  ordtypelem10  9442  oismo  9455  prlem934  10956  phimullem  16749  prmreclem5  16891  psssdm2  18547  sylow3lem3  19604  ablfacrp  20043  isdrng2  20720  fidomndrng  20750  imadrhmcl  20774  pjfo  21695  obs2ss  21709  frlmsslsp  21776  mplbas2  22020  restfpw  23144  2ndcsep  23424  ptclsg  23580  trfg  23856  restutopopn  24203  unirnblps  24384  unirnbl  24385  clsocv  25217  rrxbasefi  25377  pjth  25406  opnmbllem  25568  dvidlem  25882  dvaddf  25909  dvmulf  25910  dvcof  25915  dvcj  25917  dvrec  25922  dvcnv  25944  dvcnvre  25986  ftc1cn  26010  ulmdv  26368  pserdv  26394  ppisval2  27068  noseqrdgfn  28298  nbupgruvtxres  29476  ply1degltdimlem  33766  dimkerim  33771  fedgmul  33775  assafld  33781  extdgfialg  33838  reff  33983  dya2iocuni  34427  cvmsss2  35456  opnmbllem0  37977  ftc1cnnc  38013  lkrlsp  39548  cdleme50rnlem  40990  hdmaprnN  42310  hgmaprnN  42347  qsalrel  42680  kercvrlsm  43511  pwssplit4  43517  hbtlem5  43556  restuni3  45548  disjf1o  45621  unirnmapsn  45643  iunmapsn  45646  icoiccdif  45954  iccdificc  45969  lptioo2  46061  lptioo1  46062  qndenserrn  46727  intsaluni  46757  iundjiun  46888  meadjiunlem  46893  meaiininclem  46914  iunhoiioo  47104