Theorem eqelssd 3934

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  ordtypelem9  9544  ordtypelem10  9545  oismo  9558  prlem934  11142  phimullem  16982  prmreclem5  17124  psssdm2  18781  sylow3lem3  19870  ablfacrp  20309  isdrng2  21024  fidomndrng  21058  imadrhmcl  21081  pjfo  22048  obs2ss  22062  frlmsslsp  22129  mplbas2  22378  restfpw  23524  2ndcsep  23805  ptclsg  23961  trfg  24237  restutopopn  24584  unirnblps  24765  unirnbl  24766  clsocv  25598  rrxbasefi  25758  pjth  25787  opnmbllem  25949  dvidlem  26262  dvaddf  26289  dvmulf  26290  dvcof  26295  dvcj  26297  dvrec  26302  dvcnv  26324  dvcnvre  26366  ftc1cn  26390  ulmdv  26757  pserdv  26783  ppisval2  27459  noseqrdgfn  28719  nbupgruvtxres  30015  ply1degltdimlem  34321  dimkerim  34326  fedgmul  34330  assafld  34336  extdgfialg  34393  reff  34538  dya2iocuni  34982  cvmsss2  36205  opnmbllem0  38765  ftc1cnnc  38801  lkrlsp  40350  cdleme50rnlem  41792  hdmaprnN  43112  hgmaprnN  43149  qsalrel  43483  kercvrlsm  44276  pwssplit4  44282  hbtlem5  44320  restuni3  46336  disjf1o  46409  unirnmapsn  46430  iunmapsn  46433  icoiccdif  46739  iccdificc  46754  lptioo2  46846  lptioo1  46847  qndenserrn  47512  intsaluni  47542  iundjiun  47673  meadjiunlem  47678  meaiininclem  47699  iunhoiioo  47889  tmachlem-exlargecover  48157