Theorem dfss2 3557

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 3555	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
2		df-in 3547	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3	2	eqeq2i 2622	. . 3 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)})
4		abeq2 2719	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
5	1, 3, 4	3bitri 285	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6		pm4.71 660	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
7	6	albii 1737	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	5, 7	bitr4i 266	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977  {cab 2596   ∩ cin 3539   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  dfss3  3558  dfss2f  3559  ssel  3562  ssriv  3572  ssrdv  3574  sstr2  3575  eqss  3583  nss  3626  rabss2  3648  ssconb  3705  ssequn1  3745  unss  3749  ssin  3797  ssdif0  3896  difin0ss  3900  inssdif0  3901  reldisj  3972  ssundif  4004  sbcssg  4035  pwss  4123  snss  4259  pwpw0  4284  pwsnALT  4367  ssuni  4395  ssuniOLD  4396  unissb  4405  iunss  4497  dftr2  4682  axpweq  4768  axpow2  4771  ssextss  4849  ssrel  5130  ssrelOLD  5131  ssrel2  5133  ssrelrel  5143  reliun  5162  relop  5194  issref  5428  funimass4  6157  dfom2  6959  inf2  8403  grothpw  9527  grothprim  9535  psslinpr  9732  ltaddpr  9735  isprm2  15233  vdwmc2  15521  acsmapd  17001  dfcon2  21032  iskgen3  21162  metcld  22912  metcld2  22913  isch2  27464  pjnormssi  28411  ssiun3  28759  ssrelf  28805  bnj1361  30153  bnj978  30273  dffr5  30896  brsset  31166  sscoid  31190  relowlpssretop  32388  rp-fakeinunass  36880  rababg  36898  ss2iundf  36970  dfss6  37082  dfhe3  37089  snhesn  37100  dffrege76  37253  ntrneiiso  37409  ntrneik2  37410  ntrneix2  37411  ntrneikb  37412  conss34OLD  37667  sbcssOLD  37777  onfrALTlem2  37782  trsspwALT  38067  trsspwALT2  38068  snssiALTVD  38084  snssiALT  38085  sstrALT2VD  38091  sstrALT2  38092  sbcssgVD  38141  onfrALTlem2VD  38147  sspwimp  38176  sspwimpVD  38177  sspwimpcf  38178  sspwimpcfVD  38179  sspwimpALT  38183  unisnALT  38184  iunssf  38290  icccncfext  38773