Theorem dfss2 3624

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 3622	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
2		df-in 3614	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3	2	eqeq2i 2663	. . 3 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)})
4		abeq2 2761	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
5	1, 3, 4	3bitri 286	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6		pm4.71 663	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
7	6	albii 1787	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	5, 7	bitr4i 267	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521   = wceq 1523   ∈ wcel 2030  {cab 2637   ∩ cin 3606   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621

This theorem is referenced by:  dfss3  3625  dfss6  3626  dfss2f  3627  ssel  3630  ssriv  3640  ssrdv  3642  sstr2  3643  eqss  3651  nss  3696  rabss2  3718  ssconb  3776  ssequn1  3816  unss  3820  ssin  3868  ssdif0  3975  difin0ss  3979  inssdif0  3980  reldisj  4053  ssundif  4085  sbcssg  4118  pwss  4208  snssg  4347  pwpw0  4376  pwsnALT  4461  ssuni  4491  ssuniOLD  4492  unissb  4501  iunss  4593  dftr2  4787  axpweq  4872  axpow2  4875  ssextss  4952  ssrel  5241  ssrelOLD  5242  ssrel2  5244  ssrelrel  5254  reliun  5272  relop  5305  issref  5544  funimass4  6286  dfom2  7109  inf2  8558  grothpw  9686  grothprim  9694  psslinpr  9891  ltaddpr  9894  isprm2  15442  vdwmc2  15730  acsmapd  17225  dfconn2  21270  iskgen3  21400  metcld  23150  metcld2  23151  isch2  28208  pjnormssi  29155  ssiun3  29502  ssrelf  29553  bnj1361  31025  bnj978  31145  dffr5  31769  brsset  32121  sscoid  32145  relowlpssretop  33342  rp-fakeinunass  38178  rababg  38196  ss2iundf  38268  dfhe3  38386  snhesn  38397  dffrege76  38550  ntrneiiso  38706  ntrneik2  38707  ntrneix2  38708  ntrneikb  38709  conss34OLD  38963  sbcssOLD  39073  onfrALTlem2  39078  trsspwALT  39362  trsspwALT2  39363  snssiALTVD  39376  snssiALT  39377  sstrALT2VD  39383  sstrALT2  39384  sbcssgVD  39433  onfrALTlem2VD  39439  sspwimp  39468  sspwimpVD  39469  sspwimpcf  39470  sspwimpcfVD  39471  sspwimpALT  39475  unisnALT  39476  iunssf  39577  icccncfext  40418