Theorem eltop2 18592

Description: Membership in a topology. (Contributed by NM, 19-Jul-2006.)

Assertion

Ref	Expression
eltop2	|- ( J e. Top -> ( A e. J <-> A. x e. A E. y e. J ( x e. y /\ y C_ A ) ) )

Distinct variable groups:   x, y, A   x, J, y

Proof of Theorem eltop2

Step	Hyp	Ref	Expression
1		tgtop 18590	. . 3 |- ( J e. Top -> ( topGen ` J ) = J )
2	1	eleq2d 2510	. 2 |- ( J e. Top -> ( A e. ( topGen ` J ) <-> A e. J ) )
3		eltg2b 18576	. 2 |- ( J e. Top -> ( A e. ( topGen ` J ) <-> A. x e. A E. y e. J ( x e. y /\ y C_ A ) ) )
4	2, 3	bitr3d 255	1 |- ( J e. Top -> ( A e. J <-> A. x e. A E. y e. J ( x e. y /\ y C_ A ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   e. wcel 1756   A.wral 2727   E.wrex 2728   C_ wss 3340   ` cfv 5430   topGenctg 14388   Topctop 18510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-iota 5393  df-fun 5432  df-fv 5438  df-topgen 14394  df-top 18515

This theorem is referenced by:  isclo  18703  cncnp  18896  ist1-2  18963  hauscmp  19022  llycmpkgen2  19135  ptpjopn  19197  txkgen  19237  xkococn  19245  xkoinjcn  19272  fclscf  19610  subgntr  19689  opnsubg  19690  divstgpopn  19702  prdsxmslem2  20116  zdis  20405  efopn  22115  cvmopnlem  27179  neibastop3  28595