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

Theorem opelxp 4537
Description: Ordered pair membership in a cross product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opelxp  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )

Proof of Theorem opelxp
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp2 4525 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
2 vex 2661 . . . . . . 7  |-  x  e. 
_V
3 vex 2661 . . . . . . 7  |-  y  e. 
_V
42, 3opth2 4130 . . . . . 6  |-  ( <. A ,  B >.  = 
<. x ,  y >.  <->  ( A  =  x  /\  B  =  y )
)
5 eleq1 2178 . . . . . . 7  |-  ( A  =  x  ->  ( A  e.  C  <->  x  e.  C ) )
6 eleq1 2178 . . . . . . 7  |-  ( B  =  y  ->  ( B  e.  D  <->  y  e.  D ) )
75, 6bi2anan9 578 . . . . . 6  |-  ( ( A  =  x  /\  B  =  y )  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
84, 7sylbi 120 . . . . 5  |-  ( <. A ,  B >.  = 
<. x ,  y >.  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
98biimprcd 159 . . . 4  |-  ( ( x  e.  C  /\  y  e.  D )  ->  ( <. A ,  B >.  =  <. x ,  y
>.  ->  ( A  e.  C  /\  B  e.  D ) ) )
109rexlimivv 2530 . . 3  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  ->  ( A  e.  C  /\  B  e.  D )
)
11 eqid 2115 . . . 4  |-  <. A ,  B >.  =  <. A ,  B >.
12 opeq1 3673 . . . . . 6  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
1312eqeq2d 2127 . . . . 5  |-  ( x  =  A  ->  ( <. A ,  B >.  = 
<. x ,  y >.  <->  <. A ,  B >.  = 
<. A ,  y >.
) )
14 opeq2 3674 . . . . . 6  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
1514eqeq2d 2127 . . . . 5  |-  ( y  =  B  ->  ( <. A ,  B >.  = 
<. A ,  y >.  <->  <. A ,  B >.  = 
<. A ,  B >. ) )
1613, 15rspc2ev 2776 . . . 4  |-  ( ( A  e.  C  /\  B  e.  D  /\  <. A ,  B >.  = 
<. A ,  B >. )  ->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
1711, 16mp3an3 1287 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  ->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
1810, 17impbii 125 . 2  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  <->  ( A  e.  C  /\  B  e.  D ) )
191, 18bitri 183 1  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104    = wceq 1314    e. wcel 1463   E.wrex 2392   <.cop 3498    X. cxp 4505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-opab 3958  df-xp 4513
This theorem is referenced by:  brxp  4538  opelxpi  4539  opelxp1  4541  opelxp2  4542  opthprc  4558  elxp3  4561  opeliunxp  4562  optocl  4583  xpiindim  4644  opelres  4792  resiexg  4832  codir  4895  qfto  4896  xpmlem  4927  rnxpid  4941  ssrnres  4949  dfco2  5006  relssdmrn  5027  ressn  5047  opelf  5262  fnovex  5770  oprab4  5808  resoprab  5833  elmpocl  5934  fo1stresm  6025  fo2ndresm  6026  dfoprab4  6056  xporderlem  6094  f1od2  6098  brecop  6485  xpdom2  6691  djulclb  6906  djuss  6921  enq0enq  7203  enq0sym  7204  enq0tr  7206  nqnq0pi  7210  nnnq0lem1  7218  elinp  7246  genipv  7281  prsrlem1  7514  gt0srpr  7520  opelcn  7598  opelreal  7599  elreal2  7602  frecuzrdgrrn  10132  frec2uzrdg  10133  frecuzrdgrcl  10134  frecuzrdgsuc  10138  frecuzrdgrclt  10139  frecuzrdgsuctlem  10147  fisumcom2  11158  sqpweven  11759  2sqpwodd  11760  phimullem  11807  txuni2  12331  txcnp  12346  txcnmpt  12348  txdis1cn  12353  txlm  12354  xmeterval  12510  limccnp2lem  12720  limccnp2cntop  12721
  Copyright terms: Public domain W3C validator