Theorem dfss2 3964

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 2130, ax-11 2147, ax-12 2164. (Revised by SN, 16-May-2024.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfcleq 2720	. 2 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
2		dfss 3962	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3		pm4.71 557	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
4		elin 3960	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
5	4	bibi2i 337	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	bitr4i 278	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
7	6	albii 1814	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
8	1, 2, 7	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1532   = wceq 1534   ∈ wcel 2099   ∩ cin 3943   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961

This theorem is referenced by:  dfss3  3966  dfss6  3967  dfss2f  3968  ssel  3971  sselOLD  3972  ssriv  3982  ssrdv  3984  sstr2  3985  eqss  3993  nss  4042  rabss2  4071  ssconb  4133  ssequn1  4176  unss  4180  ssin  4226  ssdif0  4359  difin0ss  4364  inssdif0  4365  reldisj  4447  reldisjOLD  4448  ssundif  4483  sbcssg  4519  pwss  4621  snssb  4782  snssgOLD  4784  pwpw0  4812  ssuni  4930  unissb  4937  unissbOLD  4938  iunssf  5041  iunss  5042  dftr2  5261  axpweq  5344  axpow2  5361  ssextss  5449  ssrel  5778  ssrelOLD  5779  ssrel2  5781  ssrelrel  5792  reliun  5812  relop  5847  idrefALT  6111  funimass4  6957  dfom2  7866  inf2  9638  grothprim  10849  psslinpr  11046  ltaddpr  11049  isprm2  16644  vdwmc2  16939  acsmapd  18537  ismhp3  22054  dfconn2  23310  iskgen3  23440  metcld  25221  metcld2  25222  isch2  31020  pjnormssi  31965  ssiun3  32334  ssrelf  32388  bnj1361  34395  bnj978  34516  fineqvpow  34652  dffr5  35284  brsset  35421  sscoid  35445  relowlpssretop  36779  fvineqsneq  36827  unielss  42569  rp-fakeinunass  42868  rababg  42927  dfhe3  43128  snhesn  43139  dffrege76  43292  ntrneiiso  43444  ntrneik2  43445  ntrneix2  43446  ntrneikb  43447  expanduniss  43653  ismnuprim  43654  ismnushort  43661  onfrALTlem2  43908  trsspwALT  44180  trsspwALT2  44181  snssiALTVD  44189  snssiALT  44190  sstrALT2VD  44196  sstrALT2  44197  sbcssgVD  44245  onfrALTlem2VD  44251  sspwimp  44280  sspwimpVD  44281  sspwimpcf  44282  sspwimpcfVD  44283  sspwimpALT  44287  unisnALT  44288  icccncfext  45198