Theorem dfss2 3903

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 2139, ax-11 2156, ax-12 2173. (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 3901	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3		pm4.71 557	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
4		elin 3899	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
5	4	bibi2i 337	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	bitr4i 277	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
7	6	albii 1823	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
8	1, 2, 7	3bitr4i 302	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539   ∈ wcel 2108   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  dfss3  3905  dfss6  3906  dfss2f  3907  ssel  3910  sselOLD  3911  ssriv  3921  ssrdv  3923  sstr2  3924  eqss  3932  nss  3979  rabss2  4007  ssconb  4068  ssequn1  4110  unss  4114  ssin  4161  ssdif0  4294  difin0ss  4299  inssdif0  4300  reldisj  4382  reldisjOLD  4383  ssundif  4415  sbcssg  4451  pwss  4555  snssg  4715  pwpw0  4743  pwsnOLD  4829  ssuni  4863  unissb  4870  iunssf  4970  iunss  4971  dftr2  5189  axpweq  5282  axpow2  5285  ssextss  5363  ssrel  5683  ssrel2  5685  ssrelrel  5695  reliun  5715  relop  5748  idrefALT  6007  funimass4  6816  dfom2  7689  inf2  9311  grothprim  10521  psslinpr  10718  ltaddpr  10721  isprm2  16315  vdwmc2  16608  acsmapd  18187  ismhp3  21243  dfconn2  22478  iskgen3  22608  metcld  24375  metcld2  24376  isch2  29486  pjnormssi  30431  ssiun3  30799  ssrelf  30856  bnj1361  32708  bnj978  32829  fineqvpow  32965  dffr5  33627  brsset  34118  sscoid  34142  relowlpssretop  35462  fvineqsneq  35510  rp-fakeinunass  41020  rababg  41070  ss2iundf  41156  dfhe3  41272  snhesn  41283  dffrege76  41436  ntrneiiso  41590  ntrneik2  41591  ntrneix2  41592  ntrneikb  41593  expanduniss  41800  ismnuprim  41801  ismnushort  41808  onfrALTlem2  42055  trsspwALT  42327  trsspwALT2  42328  snssiALTVD  42336  snssiALT  42337  sstrALT2VD  42343  sstrALT2  42344  sbcssgVD  42392  onfrALTlem2VD  42398  sspwimp  42427  sspwimpVD  42428  sspwimpcf  42429  sspwimpcfVD  42430  sspwimpALT  42434  unisnALT  42435  icccncfext  43318