Theorem dfss3 3145

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1351   ∈ wcel 2148  ∀wral 2455   ⊆ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-ral 2460  df-in 3135  df-ss 3142

This theorem is referenced by:  ssrab  3233  eqsnm  3754  uni0b  3833  uni0c  3834  ssint  3859  ssiinf  3934  sspwuni  3969  dftr3  4103  tfis  4580  rninxp  5069  fnres  5329  eqfnfv3  5612  funimass3  5629  ffvresb  5676  tfrlemibxssdm  6323  tfr1onlembxssdm  6339  tfrcllembxssdm  6352  exmidontriimlem3  7217  suplocsr  7803  isbasis2g  13325  tgval2  13333  eltg2b  13336  tgss2  13361  basgen2  13363  bastop1  13365  unicld  13398  neipsm  13436  ssidcn  13492  bdss  14387