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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  wfrlem10OLD  8158  ordtypelem9  9294  ordtypelem10  9295  oismo  9308  prlem934  10798  phimullem  16489  prmreclem5  16630  psssdm2  18308  sylow3lem3  19243  ablfacrp  19678  isdrng2  20010  fidomndrng  20588  pjfo  20931  obs2ss  20945  frlmsslsp  21012  mplbas2  21252  restfpw  22339  2ndcsep  22619  ptclsg  22775  trfg  23051  restutopopn  23399  unirnblps  23581  unirnbl  23582  clsocv  24423  rrxbasefi  24583  pjth  24612  opnmbllem  24774  dvidlem  25088  dvaddf  25115  dvmulf  25116  dvcof  25121  dvcj  25123  dvrec  25128  dvcnv  25150  dvcnvre  25192  ftc1cn  25216  ulmdv  25571  pserdv  25597  ppisval2  26263  nbupgruvtxres  27783  dimkerim  31717  fedgmul  31721  reff  31798  dya2iocuni  32259  cvmsss2  33245  opnmbllem0  35822  ftc1cnnc  35858  lkrlsp  37123  cdleme50rnlem  38565  hdmaprnN  39885  hgmaprnN  39922  qsalrel  40222  kercvrlsm  40915  pwssplit4  40921  hbtlem5  40960  restuni3  42674  disjf1o  42736  unirnmapsn  42761  iunmapsn  42764  icoiccdif  43069  iccdificc  43084  lptioo2  43179  lptioo1  43180  qndenserrn  43847  intsaluni  43875  iundjiun  44005  meadjiunlem  44010  meaiininclem  44031  iunhoiioo  44221