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

Step	Hyp	Ref	Expression
1		df-xp 4681	. . 3 |- ( B X. C ) = { <. x , y >. | ( x e. B /\ y e. C ) }
2	1	eleq2i 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 ) ) )
4	2, 3	bitri 184	1 |- ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )

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