Theorem dfss3 3236

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wal 1400   ∈ wcel 2209  ∀wral 2528   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-ral 2533  df-in 3226  df-ss 3233

This theorem is used by:  ssrab  3326  eqsnm  3880  uni0b  3960  uni0c  3961  ssint  3986  ssiinf  4062  sspwuni  4097  dftr3  4233  tfis  4730  rninxp  5231  fnres  5500  eqfnfv3  5808  funimass3  5825  ffvresb  5871  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  exmidontriimlem3  7579  suplocsr  8176  4sqlem19  13208  imasaddfnlemg  13684  isbasis2g  15195  tgval2  15201  eltg2b  15204  tgss2  15229  basgen2  15231  bastop1  15233  unicld  15266  neipsm  15304  ssidcn  15360  bdss  16988