Theorem dfss2 3901

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 2142, ax-11 2158, ax-12 2175. (Revised by SN, 16-May-2024.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfcleq 2792	. 2 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
2		dfss 3899	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3		pm4.71 561	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
4		elin 3897	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
5	4	bibi2i 341	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	bitr4i 281	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
7	6	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
8	1, 2, 7	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ∩ cin 3880   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  dfss3  3903  dfss6  3904  dfss2f  3905  ssel  3908  sselOLD  3909  ssriv  3919  ssrdv  3921  sstr2  3922  eqss  3930  nss  3977  rabss2  4005  ssconb  4065  ssequn1  4107  unss  4111  ssin  4157  ssdif0  4277  difin0ss  4282  inssdif0  4283  reldisj  4359  reldisjOLD  4360  ssundif  4391  sbcssg  4421  pwss  4522  snssg  4678  pwpw0  4706  pwsnOLD  4793  ssuni  4825  unissb  4832  iunssf  4931  iunss  4932  dftr2  5138  axpweq  5230  axpow2  5233  ssextss  5311  ssrel  5621  ssrel2  5623  ssrelrel  5633  reliun  5653  relop  5685  idrefALT  5940  funimass4  6705  dfom2  7562  inf2  9070  grothprim  10245  psslinpr  10442  ltaddpr  10445  isprm2  16016  vdwmc2  16305  acsmapd  17780  dfconn2  22024  iskgen3  22154  metcld  23910  metcld2  23911  isch2  29006  pjnormssi  29951  ssiun3  30322  ssrelf  30379  bnj1361  32210  bnj978  32331  dffr5  33102  brsset  33463  sscoid  33487  relowlpssretop  34781  fvineqsneq  34829  rp-fakeinunass  40223  rababg  40273  ss2iundf  40360  dfhe3  40476  snhesn  40487  dffrege76  40640  ntrneiiso  40794  ntrneik2  40795  ntrneix2  40796  ntrneikb  40797  expanduniss  41001  ismnuprim  41002  onfrALTlem2  41252  trsspwALT  41524  trsspwALT2  41525  snssiALTVD  41533  snssiALT  41534  sstrALT2VD  41540  sstrALT2  41541  sbcssgVD  41589  onfrALTlem2VD  41595  sspwimp  41624  sspwimpVD  41625  sspwimpcf  41626  sspwimpcfVD  41627  sspwimpALT  41631  unisnALT  41632  icccncfext  42529