Theorem dfss2 3591

Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfss 3589	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
2		df-in 3581	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3	2	eqeq2i 2634	. . 3 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)})
4		abeq2 2732	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
5	1, 3, 4	3bitri 286	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6		pm4.71 662	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
7	6	albii 1747	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	5, 7	bitr4i 267	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481   = wceq 1483   ∈ wcel 1990  {cab 2608   ∩ cin 3573   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  dfss3  3592  dfss6  3593  dfss2f  3594  ssel  3597  ssriv  3607  ssrdv  3609  sstr2  3610  eqss  3618  nss  3663  rabss2  3685  ssconb  3743  ssequn1  3783  unss  3787  ssin  3835  ssdif0  3942  difin0ss  3946  inssdif0  3947  reldisj  4020  ssundif  4052  sbcssg  4085  pwss  4175  snss  4316  pwpw0  4344  pwsnALT  4429  ssuni  4459  ssuniOLD  4460  unissb  4469  iunss  4561  dftr2  4754  axpweq  4842  axpow2  4845  ssextss  4922  ssrel  5207  ssrelOLD  5208  ssrel2  5210  ssrelrel  5220  reliun  5239  relop  5272  issref  5509  funimass4  6247  dfom2  7067  inf2  8520  grothpw  9648  grothprim  9656  psslinpr  9853  ltaddpr  9856  isprm2  15395  vdwmc2  15683  acsmapd  17178  dfconn2  21222  iskgen3  21352  metcld  23104  metcld2  23105  isch2  28080  pjnormssi  29027  ssiun3  29376  ssrelf  29425  bnj1361  30899  bnj978  31019  dffr5  31643  brsset  31996  sscoid  32020  relowlpssretop  33212  rp-fakeinunass  37861  rababg  37879  ss2iundf  37951  dfhe3  38069  snhesn  38080  dffrege76  38233  ntrneiiso  38389  ntrneik2  38390  ntrneix2  38391  ntrneikb  38392  conss34OLD  38646  sbcssOLD  38756  onfrALTlem2  38761  trsspwALT  39045  trsspwALT2  39046  snssiALTVD  39062  snssiALT  39063  sstrALT2VD  39069  sstrALT2  39070  sbcssgVD  39119  onfrALTlem2VD  39125  sspwimp  39154  sspwimpVD  39155  sspwimpcf  39156  sspwimpcfVD  39157  sspwimpALT  39161  unisnALT  39162  iunssf  39263  icccncfext  40100