Theorem dfss 4095

Description: Variant of subclass definition dfss2 4094. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
dfss	⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		dfss2 4094	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		eqcom 2767	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3	1, 2	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ⊆ wss 3895   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-in 4091

This theorem is used by:  iinrab2  5027  wefrc  5644  cnvcnv  6183  ordtri2or3  6465  onelini  6482  funimass1  6623  sbthlem5  9114  dmaddpi  10979  dmmulpi  10980  smndex1bas  19111  restcldi  23497  cmpsublem  23723  ustuqtop5  24570  tgioo  25121  cphsscph  25578  mdbr3  32905  mdbr4  32906  ssmd1  32919  xrge00  33622  esumpfinvallem  34753  measxun2  34890  eulerpartgbij  35051  reprfz1  35300  tr0elw  37365  tr0el  37366  bj-ismooredr2  38124  bndss  38814  redundss3  39738  dfrcl2  44768  isotone2  45143  wfac8prim  46086  restuni4  46230  fourierdlem93  47303  sge0resplit  47510  mbfresmf  47843