Theorem dfss2 3969

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 2138, ax-11 2155, ax-12 2172. (Revised by SN, 16-May-2024.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfcleq 2726	. 2 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
2		dfss 3967	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3		pm4.71 559	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
4		elin 3965	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
5	4	bibi2i 338	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	bitr4i 278	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
7	6	albii 1822	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
8	1, 2, 7	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   = wceq 1542   ∈ wcel 2107   ∩ cin 3948   ⊆ wss 3949

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  dfss3  3971  dfss6  3972  dfss2f  3973  ssel  3976  sselOLD  3977  ssriv  3987  ssrdv  3989  sstr2  3990  eqss  3998  nss  4047  rabss2  4076  ssconb  4138  ssequn1  4181  unss  4185  ssin  4231  ssdif0  4364  difin0ss  4369  inssdif0  4370  reldisj  4452  reldisjOLD  4453  ssundif  4488  sbcssg  4524  pwss  4626  snssb  4787  snssgOLD  4789  pwpw0  4817  pwsnOLD  4902  ssuni  4937  unissb  4944  unissbOLD  4945  iunssf  5048  iunss  5049  dftr2  5268  axpweq  5349  axpow2  5366  ssextss  5454  ssrel  5783  ssrelOLD  5784  ssrel2  5786  ssrelrel  5797  reliun  5817  relop  5851  idrefALT  6113  funimass4  6957  dfom2  7857  inf2  9618  grothprim  10829  psslinpr  11026  ltaddpr  11029  isprm2  16619  vdwmc2  16912  acsmapd  18507  ismhp3  21686  dfconn2  22923  iskgen3  23053  metcld  24823  metcld2  24824  isch2  30476  pjnormssi  31421  ssiun3  31790  ssrelf  31844  bnj1361  33839  bnj978  33960  fineqvpow  34096  dffr5  34724  brsset  34861  sscoid  34885  relowlpssretop  36245  fvineqsneq  36293  unielss  41967  rp-fakeinunass  42266  rababg  42325  dfhe3  42526  snhesn  42537  dffrege76  42690  ntrneiiso  42842  ntrneik2  42843  ntrneix2  42844  ntrneikb  42845  expanduniss  43052  ismnuprim  43053  ismnushort  43060  onfrALTlem2  43307  trsspwALT  43579  trsspwALT2  43580  snssiALTVD  43588  snssiALT  43589  sstrALT2VD  43595  sstrALT2  43596  sbcssgVD  43644  onfrALTlem2VD  43650  sspwimp  43679  sspwimpVD  43680  sspwimpcf  43681  sspwimpcfVD  43682  sspwimpALT  43686  unisnALT  43687  icccncfext  44603