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

Theorem opelxp 4613
 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

Proof of Theorem opelxp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp2 4601 . 2
2 vex 2715 . . . . . . 7
3 vex 2715 . . . . . . 7
42, 3opth2 4199 . . . . . 6
5 eleq1 2220 . . . . . . 7
6 eleq1 2220 . . . . . . 7
75, 6bi2anan9 596 . . . . . 6
84, 7sylbi 120 . . . . 5
98biimprcd 159 . . . 4
109rexlimivv 2580 . . 3
11 eqid 2157 . . . 4
12 opeq1 3741 . . . . . 6
1312eqeq2d 2169 . . . . 5
14 opeq2 3742 . . . . . 6
1514eqeq2d 2169 . . . . 5
1613, 15rspc2ev 2831 . . . 4
1711, 16mp3an3 1308 . . 3
1810, 17impbii 125 . 2
191, 18bitri 183 1
 Colors of variables: wff set class Syntax hints:   wa 103   wb 104   wceq 1335   wcel 2128  wrex 2436  cop 3563   cxp 4581 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 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-opab 4026  df-xp 4589 This theorem is referenced by:  brxp  4614  opelxpi  4615  opelxp1  4617  opelxp2  4618  opthprc  4634  elxp3  4637  opeliunxp  4638  optocl  4659  xpiindim  4720  opelres  4868  resiexg  4908  codir  4971  qfto  4972  xpmlem  5003  rnxpid  5017  ssrnres  5025  dfco2  5082  relssdmrn  5103  ressn  5123  opelf  5338  fnovex  5848  oprab4  5886  resoprab  5911  elmpocl  6012  fo1stresm  6103  fo2ndresm  6104  dfoprab4  6134  xporderlem  6172  f1od2  6176  brecop  6563  xpdom2  6769  djulclb  6989  djuss  7004  enq0enq  7334  enq0sym  7335  enq0tr  7337  nqnq0pi  7341  nnnq0lem1  7349  elinp  7377  genipv  7412  prsrlem1  7645  gt0srpr  7651  opelcn  7729  opelreal  7730  elreal2  7733  frecuzrdgrrn  10289  frec2uzrdg  10290  frecuzrdgrcl  10291  frecuzrdgsuc  10295  frecuzrdgrclt  10296  frecuzrdgsuctlem  10304  fisumcom2  11317  fprodcom2fi  11505  sqpweven  12029  2sqpwodd  12030  phimullem  12077  txuni2  12616  txcnp  12631  txcnmpt  12633  txdis1cn  12638  txlm  12639  xmeterval  12795  limccnp2lem  13005  limccnp2cntop  13006
 Copyright terms: Public domain W3C validator