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

Theorem opelxp 4457
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 4446 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
2 vex 2622 . . . . . . 7  |-  x  e. 
_V
3 vex 2622 . . . . . . 7  |-  y  e. 
_V
42, 3opth2 4058 . . . . . 6  |-  ( <. A ,  B >.  = 
<. x ,  y >.  <->  ( A  =  x  /\  B  =  y )
)
5 eleq1 2150 . . . . . . 7  |-  ( A  =  x  ->  ( A  e.  C  <->  x  e.  C ) )
6 eleq1 2150 . . . . . . 7  |-  ( B  =  y  ->  ( B  e.  D  <->  y  e.  D ) )
75, 6bi2anan9 573 . . . . . 6  |-  ( ( A  =  x  /\  B  =  y )  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
84, 7sylbi 119 . . . . 5  |-  ( <. A ,  B >.  = 
<. x ,  y >.  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
98biimprcd 158 . . . 4  |-  ( ( x  e.  C  /\  y  e.  D )  ->  ( <. A ,  B >.  =  <. x ,  y
>.  ->  ( A  e.  C  /\  B  e.  D ) ) )
109rexlimivv 2494 . . 3  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  ->  ( A  e.  C  /\  B  e.  D )
)
11 eqid 2088 . . . 4  |-  <. A ,  B >.  =  <. A ,  B >.
12 opeq1 3617 . . . . . 6  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
1312eqeq2d 2099 . . . . 5  |-  ( x  =  A  ->  ( <. A ,  B >.  = 
<. x ,  y >.  <->  <. A ,  B >.  = 
<. A ,  y >.
) )
14 opeq2 3618 . . . . . 6  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
1514eqeq2d 2099 . . . . 5  |-  ( y  =  B  ->  ( <. A ,  B >.  = 
<. A ,  y >.  <->  <. A ,  B >.  = 
<. A ,  B >. ) )
1613, 15rspc2ev 2735 . . . 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 1262 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  ->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
1810, 17impbii 124 . 2  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  <->  ( A  e.  C  /\  B  e.  D ) )
191, 18bitri 182 1  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103    = wceq 1289    e. wcel 1438   E.wrex 2360   <.cop 3444    X. cxp 4426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-opab 3892  df-xp 4434
This theorem is referenced by:  brxp  4458  opelxpi  4459  opelxp1  4460  opelxp2  4461  opthprc  4477  elxp3  4480  opeliunxp  4481  optocl  4502  xpiindim  4561  opelres  4706  resiexg  4744  codir  4807  qfto  4808  xpmlem  4839  rnxpid  4852  ssrnres  4860  dfco2  4917  relssdmrn  4938  ressn  4958  opelf  5167  fnovex  5664  oprab4  5701  resoprab  5723  elmpt2cl  5824  fo1stresm  5914  fo2ndresm  5915  dfoprab4  5944  xporderlem  5978  f1od2  5982  brecop  6362  xpdom2  6527  djulclb  6726  djuss  6740  enq0enq  6969  enq0sym  6970  enq0tr  6972  nqnq0pi  6976  nnnq0lem1  6984  elinp  7012  genipv  7047  prsrlem1  7267  gt0srpr  7273  opelcn  7343  opelreal  7344  elreal2  7347  frecuzrdgrrn  9780  frec2uzrdg  9781  frecuzrdgrcl  9782  frecuzrdgsuc  9786  frecuzrdgrclt  9787  frecuzrdgsuctlem  9795  fisumcom2  10795  sqpweven  11246  2sqpwodd  11247  phimullem  11294
  Copyright terms: Public domain W3C validator