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

Theorem opelxp 4374
 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 4363 . 2
2 vex 2560 . . . . . . 7
3 vex 2560 . . . . . . 7
42, 3opth2 3977 . . . . . 6
5 eleq1 2100 . . . . . . 7
6 eleq1 2100 . . . . . . 7
75, 6bi2anan9 538 . . . . . 6
84, 7sylbi 114 . . . . 5
98biimprcd 149 . . . 4
109rexlimivv 2438 . . 3
11 eqid 2040 . . . 4
12 opeq1 3549 . . . . . 6
1312eqeq2d 2051 . . . . 5
14 opeq2 3550 . . . . . 6
1514eqeq2d 2051 . . . . 5
1613, 15rspc2ev 2664 . . . 4
1711, 16mp3an3 1221 . . 3
1810, 17impbii 117 . 2
191, 18bitri 173 1
 Colors of variables: wff set class Syntax hints:   wa 97   wb 98   wceq 1243   wcel 1393  wrex 2307  cop 3378   cxp 4343 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 3875  ax-pow 3927  ax-pr 3944 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 2311  df-rex 2312  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-opab 3819  df-xp 4351 This theorem is referenced by:  brxp  4375  opelxpi  4376  opelxp1  4377  opelxp2  4378  opthprc  4391  elxp3  4394  opeliunxp  4395  optocl  4416  xpiindim  4473  opelres  4617  resiexg  4653  codir  4713  qfto  4714  xpmlem  4744  rnxpid  4755  ssrnres  4763  dfco2  4820  relssdmrn  4841  ressn  4858  opelf  5062  fnovex  5538  oprab4  5575  resoprab  5597  elmpt2cl  5698  fo1stresm  5788  fo2ndresm  5789  dfoprab4  5818  xporderlem  5852  brecop  6196  xpdom2  6305  enq0enq  6529  enq0sym  6530  enq0tr  6532  nqnq0pi  6536  nnnq0lem1  6544  elinp  6572  genipv  6607  prsrlem1  6827  gt0srpr  6833  opelcn  6903  opelreal  6904  elreal2  6907  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgrom  9196  frecuzrdgsuc  9201
 Copyright terms: Public domain W3C validator