Theorem eqelssd 3991

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113   ⊆ wss 3939

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-in 3946  df-ss 3955

This theorem is referenced by:  wfrlem10  7967  ordtypelem9  8993  ordtypelem10  8994  oismo  9007  prlem934  10458  phimullem  16119  prmreclem5  16259  psssdm2  17828  sylow3lem3  18757  ablfacrp  19191  isdrng2  19515  fidomndrng  20083  mplbas2  20254  pjfo  20862  obs2ss  20876  frlmsslsp  20943  restfpw  21790  2ndcsep  22070  ptclsg  22226  trfg  22502  restutopopn  22850  unirnblps  23032  unirnbl  23033  clsocv  23856  rrxbasefi  24016  pjth  24045  opnmbllem  24205  dvidlem  24516  dvaddf  24542  dvmulf  24543  dvcof  24548  dvcj  24550  dvrec  24555  dvcnv  24577  dvcnvre  24619  ftc1cn  24643  ulmdv  24994  pserdv  25020  ppisval2  25685  nbupgruvtxres  27192  dimkerim  31027  fedgmul  31031  reff  31107  dya2iocuni  31545  cvmsss2  32525  opnmbllem0  34932  ftc1cnnc  34970  lkrlsp  36242  cdleme50rnlem  37684  hdmaprnN  39004  hgmaprnN  39041  qsalrel  39131  kercvrlsm  39689  pwssplit4  39695  hbtlem5  39734  restuni3  41390  disjf1o  41458  unirnmapsn  41483  iunmapsn  41486  icoiccdif  41806  iccdificc  41821  lptioo2  41918  lptioo1  41919  qndenserrn  42591  intsaluni  42619  iundjiun  42749  meadjiunlem  42754  meaiininclem  42775  iunhoiioo  42965