Theorem eqelssd 3911

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 3897	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
5	1, 4	eqssd 3908	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2080   ⊆ wss 3861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-in 3868  df-ss 3876

This theorem is referenced by:  wfrlem10  7819  ordtypelem9  8839  ordtypelem10  8840  oismo  8853  prlem934  10304  phimullem  15945  prmreclem5  16085  psssdm2  17654  sylow3lem3  18484  ablfacrp  18905  isdrng2  19202  fidomndrng  19769  mplbas2  19938  pjfo  20541  obs2ss  20555  frlmsslsp  20622  restfpw  21471  2ndcsep  21751  ptclsg  21907  trfg  22183  restutopopn  22530  unirnblps  22712  unirnbl  22713  clsocv  23536  rrxbasefi  23696  pjth  23725  opnmbllem  23885  dvidlem  24196  dvaddf  24222  dvmulf  24223  dvcof  24228  dvcj  24230  dvrec  24235  dvcnv  24257  dvcnvre  24299  ftc1cn  24323  ulmdv  24674  pserdv  24700  ppisval2  25364  nbupgruvtxres  26872  dimkerim  30619  fedgmul  30623  reff  30712  dya2iocuni  31150  cvmsss2  32123  opnmbllem0  34472  ftc1cnnc  34510  lkrlsp  35782  cdleme50rnlem  37224  hdmaprnN  38544  hgmaprnN  38581  kercvrlsm  39181  pwssplit4  39187  hbtlem5  39226  restuni3  40937  disjf1o  41005  unirnmapsn  41030  iunmapsn  41033  icoiccdif  41355  iccdificc  41370  lptioo2  41467  lptioo1  41468  qndenserrn  42140  intsaluni  42168  iundjiun  42298  meadjiunlem  42303  meaiininclem  42324  iunhoiioo  42514