Theorem dfss2 3907

Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.) Avoid ax-10 2137, ax-11 2154, ax-12 2171. (Revised by SN, 16-May-2024.)

Assertion

Ref	Expression
dfss2	⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfcleq 2731	. 2 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
2		dfss 3905	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3		pm4.71 558	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
4		elin 3903	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
5	4	bibi2i 338	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	bitr4i 277	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
7	6	albii 1822	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
8	1, 2, 7	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539   ∈ wcel 2106   ∩ cin 3886   ⊆ wss 3887

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  dfss3  3909  dfss6  3910  dfss2f  3911  ssel  3914  sselOLD  3915  ssriv  3925  ssrdv  3927  sstr2  3928  eqss  3936  nss  3983  rabss2  4011  ssconb  4072  ssequn1  4114  unss  4118  ssin  4164  ssdif0  4297  difin0ss  4302  inssdif0  4303  reldisj  4385  reldisjOLD  4386  ssundif  4418  sbcssg  4454  pwss  4558  snssg  4718  pwpw0  4746  pwsnOLD  4832  ssuni  4866  unissb  4873  iunssf  4974  iunss  4975  dftr2  5193  axpweq  5287  axpow2  5290  ssextss  5369  ssrel  5693  ssrelOLD  5694  ssrel2  5696  ssrelrel  5706  reliun  5726  relop  5759  idrefALT  6018  funimass4  6834  dfom2  7714  inf2  9381  grothprim  10590  psslinpr  10787  ltaddpr  10790  isprm2  16387  vdwmc2  16680  acsmapd  18272  ismhp3  21333  dfconn2  22570  iskgen3  22700  metcld  24470  metcld2  24471  isch2  29585  pjnormssi  30530  ssiun3  30898  ssrelf  30955  bnj1361  32808  bnj978  32929  fineqvpow  33065  dffr5  33721  brsset  34191  sscoid  34215  relowlpssretop  35535  fvineqsneq  35583  rp-fakeinunass  41122  rababg  41181  ss2iundf  41267  dfhe3  41383  snhesn  41394  dffrege76  41547  ntrneiiso  41701  ntrneik2  41702  ntrneix2  41703  ntrneikb  41704  expanduniss  41911  ismnuprim  41912  ismnushort  41919  onfrALTlem2  42166  trsspwALT  42438  trsspwALT2  42439  snssiALTVD  42447  snssiALT  42448  sstrALT2VD  42454  sstrALT2  42455  sbcssgVD  42503  onfrALTlem2VD  42509  sspwimp  42538  sspwimpVD  42539  sspwimpcf  42540  sspwimpcfVD  42541  sspwimpALT  42545  unisnALT  42546  icccncfext  43428