Theorem dfss3 3169

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 3168	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		df-ral 2477	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	1, 2	bitr4i 187	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1362   ∈ wcel 2164  ∀wral 2472   ⊆ wss 3153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-ral 2477  df-in 3159  df-ss 3166

This theorem is referenced by:  ssrab  3257  eqsnm  3781  uni0b  3860  uni0c  3861  ssint  3886  ssiinf  3962  sspwuni  3997  dftr3  4131  tfis  4615  rninxp  5109  fnres  5370  eqfnfv3  5657  funimass3  5674  ffvresb  5721  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  exmidontriimlem3  7283  suplocsr  7869  4sqlem19  12547  imasaddfnlemg  12897  isbasis2g  14213  tgval2  14219  eltg2b  14222  tgss2  14247  basgen2  14249  bastop1  14251  unicld  14284  neipsm  14322  ssidcn  14378  bdss  15356