Theorem dfss3 2055

Description: Alternate definition of subclass relationship.

Assertion

Ref	Expression
dfss3	|- (A (_ B <-> A.x e. A x e. B)

Distinct variable groups:   x,A   x,B

Proof of Theorem dfss3

Step	Hyp	Ref	Expression
1		dfss2 2054	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
2		df-ral 1646	. 2 |- (A.x e. A x e. B <-> A.x(x e. A -> x e. B))
3	1, 2	bitr4 176	1 |- (A (_ B <-> A.x e. A x e. B)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 952   e. wcel 956  A.wral 1642   (_ wss 2043

This theorem is referenced by:  ssrab 2121  disjssun 2322  eqsn 2470  uni0b 2518  uni0c 2519  ssint 2544  dftr3 2679  dftr4 2680  elpwunsn 2907  wefrc 2938  ordunisssuc 3078  tfis 3122  rninxp 3474  funimass3 3797  ffnfv 3819  tz9.12lem3 4641  rankval3 4661  bndrank 4662  rankonid 4675  iscard 4833  cfub 4888  cflim 4889  infxpidmlem8 7510  isbasis2g 7562  tgval2t 7567  basgent 7590  cctop 7602  intcld 7630  neips 7677  ubthlem5 8477  axgroth3 8718  blkssatm 10639

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ral 1646  df-in 2047  df-ss 2049

Copyright terms: Public domain