Theorem eqelssd 4002

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  wfrlem10OLD  8320  ordtypelem9  9523  ordtypelem10  9524  oismo  9537  prlem934  11030  phimullem  16716  prmreclem5  16857  psssdm2  18538  sylow3lem3  19538  ablfacrp  19977  isdrng2  20514  imadrhmcl  20556  fidomndrng  21126  pjfo  21489  obs2ss  21503  frlmsslsp  21570  mplbas2  21816  restfpw  22903  2ndcsep  23183  ptclsg  23339  trfg  23615  restutopopn  23963  unirnblps  24145  unirnbl  24146  clsocv  24998  rrxbasefi  25158  pjth  25187  opnmbllem  25350  dvidlem  25664  dvaddf  25693  dvmulf  25694  dvcof  25700  dvcj  25702  dvrec  25707  dvcnv  25729  dvcnvre  25771  ftc1cn  25795  ulmdv  26151  pserdv  26177  ppisval2  26845  nbupgruvtxres  28931  ply1degltdimlem  32995  dimkerim  33000  fedgmul  33004  reff  33117  dya2iocuni  33580  cvmsss2  34563  opnmbllem0  36827  ftc1cnnc  36863  lkrlsp  38275  cdleme50rnlem  39718  hdmaprnN  41038  hgmaprnN  41075  qsalrel  41368  kercvrlsm  42127  pwssplit4  42133  hbtlem5  42172  restuni3  44108  disjf1o  44188  unirnmapsn  44211  iunmapsn  44214  icoiccdif  44535  iccdificc  44550  lptioo2  44645  lptioo1  44646  qndenserrn  45313  intsaluni  45343  iundjiun  45474  meadjiunlem  45479  meaiininclem  45500  iunhoiioo  45690