Theorem dfss2 3958

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 3956	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
2		df-in 3946	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3	2	eqeq2i 2837	. . 3 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)})
4		abeq2 2948	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
5	1, 3, 4	3bitri 299	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6		pm4.71 560	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
7	6	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	5, 7	bitr4i 280	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1534   = wceq 1536   ∈ wcel 2113  {cab 2802   ∩ cin 3938   ⊆ wss 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-in 3946  df-ss 3955

This theorem is referenced by:  dfss3  3959  dfss6  3960  dfss2f  3961  ssel  3964  ssriv  3974  ssrdv  3976  sstr2  3977  eqss  3985  nss  4032  rabss2  4057  ssconb  4117  ssequn1  4159  unss  4163  ssin  4210  ssdif0  4326  difin0ss  4331  inssdif0  4332  reldisj  4405  ssundif  4436  sbcssg  4466  pwss  4567  snssg  4720  pwpw0  4749  pwsnOLD  4834  ssuni  4866  unissb  4873  iunss  4972  dftr2  5177  axpweq  5268  axpow2  5271  ssextss  5349  ssrel  5660  ssrel2  5662  ssrelrel  5672  reliun  5692  relop  5724  idrefALT  5976  funimass4  6733  dfom2  7585  inf2  9089  grothprim  10259  psslinpr  10456  ltaddpr  10459  isprm2  16029  vdwmc2  16318  acsmapd  17791  dfconn2  22030  iskgen3  22160  metcld  23912  metcld2  23913  isch2  29003  pjnormssi  29948  ssiun3  30313  ssrelf  30369  bnj1361  32104  bnj978  32225  dffr5  32993  brsset  33354  sscoid  33378  relowlpssretop  34649  fvineqsneq  34697  rp-fakeinunass  39887  rababg  39939  ss2iundf  40010  dfhe3  40127  snhesn  40138  dffrege76  40291  ntrneiiso  40447  ntrneik2  40448  ntrneix2  40449  ntrneikb  40450  expanduniss  40635  ismnuprim  40636  onfrALTlem2  40886  trsspwALT  41158  trsspwALT2  41159  snssiALTVD  41167  snssiALT  41168  sstrALT2VD  41174  sstrALT2  41175  sbcssgVD  41223  onfrALTlem2VD  41229  sspwimp  41258  sspwimpVD  41259  sspwimpcf  41260  sspwimpcfVD  41261  sspwimpALT  41265  unisnALT  41266  iunssf  41358  icccncfext  42176