ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elxp Unicode version

Theorem elxp 4692
Description: Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
elxp  |-  ( A  e.  ( B  X.  C )  <->  E. x E. y ( A  = 
<. x ,  y >.  /\  ( x  e.  B  /\  y  e.  C
) ) )
Distinct variable groups:    x, y, A   
x, B, y    x, C, y

Proof of Theorem elxp
StepHypRef Expression
1 df-xp 4681 . . 3  |-  ( B  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  C ) }
21eleq2i 2272 . 2  |-  ( A  e.  ( B  X.  C )  <->  A  e.  {
<. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } )
3 elopab 4304 . 2  |-  ( A  e.  { <. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } 
<->  E. x E. y
( A  =  <. x ,  y >.  /\  (
x  e.  B  /\  y  e.  C )
) )
42, 3bitri 184 1  |-  ( A  e.  ( B  X.  C )  <->  E. x E. y ( A  = 
<. x ,  y >.  /\  ( x  e.  B  /\  y  e.  C
) ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105    = wceq 1373   E.wex 1515    e. wcel 2176   <.cop 3636   {copab 4104    X. cxp 4673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253
This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-opab 4106  df-xp 4681
This theorem is referenced by:  elxp2  4693  0nelxp  4703  0nelelxp  4704  rabxp  4712  elxp3  4729  elvv  4737  elvvv  4738  0xp  4755  xpmlem  5103  elxp4  5170  elxp5  5171  dfco2a  5183  opabex3d  6206  opabex3  6207  xp1st  6251  xp2nd  6252  poxp  6318  xpsnen  6916  xpcomco  6921  xpassen  6925  nqnq0pi  7551  fsum2dlemstep  11745  fprod2dlemstep  11933
  Copyright terms: Public domain W3C validator