New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  risset GIF version

Theorem risset 2661
 Description: Two ways to say "A belongs to B." (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
risset (A Bx B x = A)
Distinct variable groups:   x,A   x,B

Proof of Theorem risset
StepHypRef Expression
1 exancom 1586 . 2 (x(x B x = A) ↔ x(x = A x B))
2 df-rex 2620 . 2 (x B x = Ax(x B x = A))
3 df-clel 2349 . 2 (A Bx(x = A x B))
41, 2, 33bitr4ri 269 1 (A Bx B x = A)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2615 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-clel 2349  df-rex 2620 This theorem is referenced by:  reueq  3033  reuind  3039  0el  3566  iunid  4021  snelpw1  4146  unipw1  4325  addcid1  4405  nncaddccl  4419  vfinspsslem1  4550  vfinspclt  4552  nulnnn  4556  dfproj12  4576  dfproj22  4577  proj1op  4600  proj2op  4601  phidisjnn  4615  phialllem1  4616  dfdm4  5507  dfrn5  5508  oqelins4  5794  otsnelsi3  5805  addcfnex  5824  funsex  5828  qsid  5990  mapexi  6003  xpassen  6057  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  ovcelem1  6171  ce0nn  6180  finnc  6243  nncdiv3lem1  6275  nchoicelem11  6299  nchoicelem12  6300  nchoicelem17  6305  nchoicelem18  6306
 Copyright terms: Public domain W3C validator