Theorem dfss3 2062

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 2061	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
2		df-ral 1652	. 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 956   e. wcel 960  A.wral 1648   (_ wss 2050

This theorem is referenced by:  ssrab 2128  disjssun 2330  eqsn 2478  uni0b 2527  uni0c 2528  ssint 2553  dftr3 2689  dftr4 2690  elpwunsn 2918  wefrc 2949  ordunisssuc 3089  tfis 3133  rninxp 3488  funimass3 3812  ffnfv 3834  tz9.12lem3 4671  rankval3 4691  bndrank 4692  rankonid 4705  iscard 4864  cfub 4920  cflim 4921  infxpidmlem8 7560  isbasis2g 7611  tgval2t 7616  basgent 7639  cctop 7649  intcld 7677  neips 7724  ubthlem5 8529  axgroth3 8774  blkssatm 10738

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-in 2054  df-ss 2056

Copyright terms: Public domain