Theorem eqelssd 3957

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569   ∈ wcel 2142   ⊆ wss 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-ss 3921

This theorem is used by:  ordtypelem9  9486  ordtypelem10  9487  oismo  9500  prlem934  11024  phimullem  16844  prmreclem5  16986  psssdm2  18643  sylow3lem3  19705  ablfacrp  20144  isdrng2  20854  fidomndrng  20888  imadrhmcl  20911  pjfo  21876  obs2ss  21890  frlmsslsp  21957  mplbas2  22204  restfpw  23347  2ndcsep  23627  ptclsg  23783  trfg  24059  restutopopn  24406  unirnblps  24587  unirnbl  24588  clsocv  25420  rrxbasefi  25580  pjth  25609  opnmbllem  25771  dvidlem  26085  dvaddf  26112  dvmulf  26113  dvcof  26118  dvcj  26120  dvrec  26125  dvcnv  26147  dvcnvre  26189  ftc1cn  26213  ulmdv  26577  pserdv  26603  ppisval2  27280  noseqrdgfn  28510  nbupgruvtxres  29768  ply1degltdimlem  34021  dimkerim  34026  fedgmul  34030  assafld  34036  extdgfialg  34093  reff  34238  dya2iocuni  34682  cvmsss2  35774  opnmbllem0  38335  ftc1cnnc  38371  lkrlsp  39904  cdleme50rnlem  41346  hdmaprnN  42666  hgmaprnN  42703  qsalrel  43037  kercvrlsm  43838  pwssplit4  43844  hbtlem5  43883  restuni3  45864  disjf1o  45937  unirnmapsn  45958  iunmapsn  45961  icoiccdif  46268  iccdificc  46283  lptioo2  46375  lptioo1  46376  qndenserrn  47041  intsaluni  47071  iundjiun  47202  meadjiunlem  47207  meaiininclem  47228  iunhoiioo  47418