Theorem dfss3 3118

Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss3

Step	Hyp	Ref	Expression
1		dfss2 3117	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		df-ral 2440	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	1, 2	bitr4i 186	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1333   ∈ wcel 2128  ∀wral 2435   ⊆ wss 3102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-ral 2440  df-in 3108  df-ss 3115

This theorem is referenced by:  ssrab  3206  eqsnm  3718  uni0b  3797  uni0c  3798  ssint  3823  ssiinf  3898  sspwuni  3933  dftr3  4066  tfis  4540  rninxp  5026  fnres  5283  eqfnfv3  5564  funimass3  5580  ffvresb  5627  tfrlemibxssdm  6268  tfr1onlembxssdm  6284  tfrcllembxssdm  6297  exmidontriimlem3  7141  suplocsr  7712  isbasis2g  12403  tgval2  12411  eltg2b  12414  tgss2  12439  basgen2  12441  bastop1  12443  unicld  12476  neipsm  12514  ssidcn  12570  bdss  13399