Theorem dfss2 3968

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 3966	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3		pm4.71 559	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
4		elin 3964	. . . . 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 3947   ⊆ wss 3948

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 3955  df-ss 3965

This theorem is referenced by:  dfss3  3970  dfss6  3971  dfss2f  3972  ssel  3975  sselOLD  3976  ssriv  3986  ssrdv  3988  sstr2  3989  eqss  3997  nss  4046  rabss2  4075  ssconb  4137  ssequn1  4180  unss  4184  ssin  4230  ssdif0  4363  difin0ss  4368  inssdif0  4369  reldisj  4451  reldisjOLD  4452  ssundif  4487  sbcssg  4523  pwss  4625  snssb  4786  snssgOLD  4788  pwpw0  4816  pwsnOLD  4901  ssuni  4936  unissb  4943  unissbOLD  4944  iunssf  5047  iunss  5048  dftr2  5267  axpweq  5348  axpow2  5365  ssextss  5453  ssrel  5781  ssrelOLD  5782  ssrel2  5784  ssrelrel  5795  reliun  5815  relop  5849  idrefALT  6110  funimass4  6954  dfom2  7854  inf2  9615  grothprim  10826  psslinpr  11023  ltaddpr  11026  isprm2  16616  vdwmc2  16909  acsmapd  18504  ismhp3  21678  dfconn2  22915  iskgen3  23045  metcld  24815  metcld2  24816  isch2  30464  pjnormssi  31409  ssiun3  31778  ssrelf  31832  bnj1361  33828  bnj978  33949  fineqvpow  34085  dffr5  34713  brsset  34850  sscoid  34874  relowlpssretop  36234  fvineqsneq  36282  unielss  41953  rp-fakeinunass  42252  rababg  42311  dfhe3  42512  snhesn  42523  dffrege76  42676  ntrneiiso  42828  ntrneik2  42829  ntrneix2  42830  ntrneikb  42831  expanduniss  43038  ismnuprim  43039  ismnushort  43046  onfrALTlem2  43293  trsspwALT  43565  trsspwALT2  43566  snssiALTVD  43574  snssiALT  43575  sstrALT2VD  43581  sstrALT2  43582  sbcssgVD  43630  onfrALTlem2VD  43636  sspwimp  43665  sspwimpVD  43666  sspwimpcf  43667  sspwimpcfVD  43668  sspwimpALT  43672  unisnALT  43673  icccncfext  44590