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

Theorem opelxp 4352
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 4341 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
2 vex 2557 . . . . . . 7  |-  x  e. 
_V
3 vex 2557 . . . . . . 7  |-  y  e. 
_V
42, 3opth2 3974 . . . . . 6  |-  ( <. A ,  B >.  = 
<. x ,  y >.  <->  ( A  =  x  /\  B  =  y )
)
5 eleq1 2100 . . . . . . 7  |-  ( A  =  x  ->  ( A  e.  C  <->  x  e.  C ) )
6 eleq1 2100 . . . . . . 7  |-  ( B  =  y  ->  ( B  e.  D  <->  y  e.  D ) )
75, 6bi2anan9 538 . . . . . 6  |-  ( ( A  =  x  /\  B  =  y )  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
84, 7sylbi 114 . . . . 5  |-  ( <. A ,  B >.  = 
<. x ,  y >.  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
98biimprcd 149 . . . 4  |-  ( ( x  e.  C  /\  y  e.  D )  ->  ( <. A ,  B >.  =  <. x ,  y
>.  ->  ( A  e.  C  /\  B  e.  D ) ) )
109rexlimivv 2435 . . 3  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  ->  ( A  e.  C  /\  B  e.  D )
)
11 eqid 2040 . . . 4  |-  <. A ,  B >.  =  <. A ,  B >.
12 opeq1 3546 . . . . . 6  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
1312eqeq2d 2051 . . . . 5  |-  ( x  =  A  ->  ( <. A ,  B >.  = 
<. x ,  y >.  <->  <. A ,  B >.  = 
<. A ,  y >.
) )
14 opeq2 3547 . . . . . 6  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
1514eqeq2d 2051 . . . . 5  |-  ( y  =  B  ->  ( <. A ,  B >.  = 
<. A ,  y >.  <->  <. A ,  B >.  = 
<. A ,  B >. ) )
1613, 15rspc2ev 2661 . . . 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 1221 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  ->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
1810, 17impbii 117 . 2  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  <->  ( A  e.  C  /\  B  e.  D ) )
191, 18bitri 173 1  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 97    <-> wb 98    = wceq 1243    e. wcel 1393   E.wrex 2304   <.cop 3375    X. cxp 4321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3872  ax-pow 3924  ax-pr 3941
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2308  df-rex 2309  df-v 2556  df-un 2919  df-in 2921  df-ss 2928  df-pw 3358  df-sn 3378  df-pr 3379  df-op 3381  df-opab 3816  df-xp 4329
This theorem is referenced by:  brxp  4353  opelxpi  4354  opelxp1  4355  opelxp2  4356  opthprc  4369  elxp3  4372  opeliunxp  4373  optocl  4394  xpiindim  4451  opelres  4595  resiexg  4631  codir  4691  qfto  4692  xpmlem  4722  rnxpid  4733  ssrnres  4741  dfco2  4798  relssdmrn  4819  ressn  4836  opelf  5040  fnovex  5516  oprab4  5553  resoprab  5575  elmpt2cl  5676  fo1stresm  5766  fo2ndresm  5767  dfoprab4  5796  xporderlem  5830  brecop  6174  xpdom2  6283  enq0enq  6501  enq0sym  6502  enq0tr  6504  nqnq0pi  6508  nnnq0lem1  6516  elinp  6544  genipv  6579  prsrlem1  6799  gt0srpr  6805  opelcn  6875  opelreal  6876  elreal2  6879  frecuzrdgrrn  9063  frec2uzrdg  9064  frecuzrdgrom  9065  frecuzrdgsuc  9070
  Copyright terms: Public domain W3C validator