Theorem dfss2 3918

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 2136, ax-11 2153, ax-12 2170. (Revised by SN, 16-May-2024.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfcleq 2729	. 2 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
2		dfss 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
3		pm4.71 558	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
4		elin 3914	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
5	4	bibi2i 337	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	bitr4i 277	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
7	6	albii 1820	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∩ 𝐵)))
8	1, 2, 7	3bitr4i 302	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1538   = wceq 1540   ∈ wcel 2105   ∩ cin 3897   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915

This theorem is referenced by:  dfss3  3920  dfss6  3921  dfss2f  3922  ssel  3925  sselOLD  3926  ssriv  3936  ssrdv  3938  sstr2  3939  eqss  3947  nss  3994  rabss2  4023  ssconb  4084  ssequn1  4127  unss  4131  ssin  4177  ssdif0  4310  difin0ss  4315  inssdif0  4316  reldisj  4398  reldisjOLD  4399  ssundif  4432  sbcssg  4468  pwss  4570  snssb  4730  snssgOLD  4732  pwpw0  4760  pwsnOLD  4845  ssuni  4880  unissb  4887  unissbOLD  4888  iunssf  4991  iunss  4992  dftr2  5211  axpweq  5307  axpow2  5310  ssextss  5398  ssrel  5724  ssrelOLD  5725  ssrel2  5727  ssrelrel  5738  reliun  5758  relop  5792  idrefALT  6051  funimass4  6890  dfom2  7782  inf2  9480  grothprim  10691  psslinpr  10888  ltaddpr  10891  isprm2  16484  vdwmc2  16777  acsmapd  18369  ismhp3  21439  dfconn2  22676  iskgen3  22806  metcld  24576  metcld2  24577  isch2  29873  pjnormssi  30818  ssiun3  31185  ssrelf  31242  bnj1361  33107  bnj978  33228  fineqvpow  33364  dffr5  34010  brsset  34287  sscoid  34311  relowlpssretop  35648  fvineqsneq  35696  rp-fakeinunass  41452  rababg  41511  dfhe3  41712  snhesn  41723  dffrege76  41876  ntrneiiso  42030  ntrneik2  42031  ntrneix2  42032  ntrneikb  42033  expanduniss  42240  ismnuprim  42241  ismnushort  42248  onfrALTlem2  42495  trsspwALT  42767  trsspwALT2  42768  snssiALTVD  42776  snssiALT  42777  sstrALT2VD  42783  sstrALT2  42784  sbcssgVD  42832  onfrALTlem2VD  42838  sspwimp  42867  sspwimpVD  42868  sspwimpcf  42869  sspwimpcfVD  42870  sspwimpALT  42874  unisnALT  42875  icccncfext  43772