Theorem dfss3 1498

Description: Alternate definition of subclass relationship.

Assertion

Ref	Expression
dfss3	⊢ (A ⊆ B ↔ ∀x ∈ A x ∈ B)

Distinct variable group(s):   x,A   x,B

Proof of Theorem dfss3

Step	Hyp	Ref	Expression
1		dfss2 1497	. 2 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
2		df-ral 1205	. 2 ⊢ (∀x ∈ A x ∈ B ↔ ∀x(x ∈ A → x ∈ B))
3	1, 2	bitr4 154	1 ⊢ (A ⊆ B ↔ ∀x ∈ A x ∈ B)

Syntax hints:   → wi 2   ↔ wb 127  ∀wal 672   ∈ wcel 1092  ∀wral 1201   ⊆ wss 1487

This theorem is referenced by:  uni0b 1939  ssint 1980  dftr3 2045  dftr4 2046  wefrc 2195  tfis 2245  ordunisssuc 2334  ffnfv 2892  tz9.12lem3 3505  rankval3 3525  bndrank 3526  rankonid 3538  iscard 3659  cfub 3703  cflim 3704  infxpidmlem8 4940

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-in 1491  df-ss 1492

metamath.org