Theorem dfss2 3809

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 3807	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
2		df-in 3799	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3	2	eqeq2i 2790	. . 3 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)})
4		abeq2 2892	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
5	1, 3, 4	3bitri 289	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6		pm4.71 553	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
7	6	albii 1863	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	5, 7	bitr4i 270	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386  ∀wal 1599   = wceq 1601   ∈ wcel 2107  {cab 2763   ∩ cin 3791   ⊆ wss 3792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-in 3799  df-ss 3806

This theorem is referenced by:  dfss3  3810  dfss6  3811  dfss2f  3812  ssel  3815  ssriv  3825  ssrdv  3827  sstr2  3828  eqss  3836  nss  3882  rabss2  3906  ssconb  3966  ssequn1  4006  unss  4010  ssin  4055  ssdif0  4172  difin0ss  4177  inssdif0  4178  reldisj  4245  ssundif  4276  sbcssg  4306  pwss  4396  snssg  4548  pwpw0  4577  pwsnALT  4666  ssuni  4697  unissb  4706  iunss  4796  dftr2  4991  axpweq  5078  axpow2  5081  ssextss  5156  ssrel  5457  ssrel2  5459  ssrelrel  5469  reliun  5489  relop  5520  idrefALT  5765  idrefOLD  5766  funimass4  6509  dfom2  7347  inf2  8819  grothprim  9993  psslinpr  10190  ltaddpr  10193  isprm2  15804  vdwmc2  16091  acsmapd  17568  dfconn2  21635  iskgen3  21765  metcld  23516  metcld2  23517  isch2  28656  pjnormssi  29603  ssiun3  29942  ssrelf  29994  bnj1361  31502  bnj978  31622  dffr5  32241  brsset  32589  sscoid  32613  relowlpssretop  33810  rp-fakeinunass  38828  rababg  38846  ss2iundf  38918  dfhe3  39035  snhesn  39046  dffrege76  39199  ntrneiiso  39355  ntrneik2  39356  ntrneix2  39357  ntrneikb  39358  onfrALTlem2  39716  trsspwALT  39997  trsspwALT2  39998  snssiALTVD  40006  snssiALT  40007  sstrALT2VD  40013  sstrALT2  40014  sbcssgVD  40062  onfrALTlem2VD  40068  sspwimp  40097  sspwimpVD  40098  sspwimpcf  40099  sspwimpcfVD  40100  sspwimpALT  40104  unisnALT  40105  iunssf  40204  icccncfext  41038