MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opelxpi Structured version   Visualization version   GIF version

Theorem opelxpi 5591
Description: Ordered pair membership in a Cartesian product (implication). (Contributed by NM, 28-May-1995.)
Assertion
Ref Expression
opelxpi ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpi
StepHypRef Expression
1 opelxp 5590 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 229 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  cop 4570   × cxp 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-opab 5126  df-xp 5560
This theorem is referenced by:  opelxpd  5592  opelvv  5593  opelvvg  5594  opbrop  5647  elsnxp  6141  reuop  6143  fnbrfvb2  6721  ov3  7305  ovres  7308  fovrn  7312  fnovrn  7317  ovima0  7321  ovconst2  7322  el2xptp0  7732  opiota  7753  fimaproj  7825  seqomlem2  8083  brdifun  8313  ecopqsi  8349  brecop  8385  eceqoveq  8397  xpcomco  8601  djulcl  9333  djurcl  9334  djulf1o  9335  djurf1o  9336  djuun  9349  isfin4p1  9731  axdc4lem  9871  canthp1lem2  10069  addpiord  10300  mulpiord  10301  pinq  10343  nqereu  10345  addpipq  10353  addpqnq  10354  mulpipq  10356  mulpqnq  10357  ordpipq  10358  recmulnq  10380  dmrecnq  10384  enreceq  10482  addsrpr  10491  mulsrpr  10492  0r  10496  1sr  10497  m1r  10498  addclsr  10499  mulclsr  10500  axaddf  10561  xrlenlt  10700  uzrdgfni  13321  swrdval  14000  ruclem6  15583  eucalgf  15922  eucalg  15926  qnumdenbi  16079  setscom  16522  strfv2d  16524  setsid  16533  imasaddfnlem  16796  imasaddflem  16798  imasvscafn  16805  imasvscaval  16806  funcpropd  17165  fucco  17227  catcxpccl  17452  curf1cl  17473  curf2cl  17476  curfcl  17477  uncfcurf  17484  diag2  17490  curf2ndf  17492  joindmss  17612  meetdmss  17626  latlem  17654  latjcom  17664  latmcom  17680  efgmf  18775  efglem  18778  vrgpf  18830  vrgpinv  18831  frgpuplem  18834  frgpup2  18838  frgpnabllem1  18929  gsumxp2  19036  mamudi  20947  mamudir  20948  mamuvs1  20949  mamuvs2  20950  matsubgcell  20978  matvscacell  20980  pmatcoe1fsupp  21244  txbas  22110  txcls  22147  upxp  22166  uptx  22168  txtube  22183  txcmplem1  22184  txlm  22191  tx1stc  22193  txkgen  22195  cnmpt21  22214  txswaphmeolem  22347  txswaphmeo  22348  clssubg  22651  qustgplem  22663  comet  23057  txmetcnp  23091  metustsym  23099  nrmmetd  23118  isngp3  23141  ngpds  23147  qtopbaslem  23301  cnmetdval  23313  remetdval  23331  tgqioo  23342  bndth  23496  htpyco2  23517  phtpyco2  23528  ovolicc1  24051  ioorf  24108  ioorcl  24112  itg1addlem4  24234  dvcnp2  24451  dvef  24511  lhop1lem  24544  taylthlem2  24896  addsqnreup  25952  brcgr  26619  ex-fpar  28174  imsdval  28396  sspval  28433  opreu2reuALT  30173  ofoprabco  30343  f1od2  30389  qtophaus  31005  mbfmco2  31428  eulerpartlemgh  31541  afsval  31847  erdszelem9  32349  cvmlift2lem1  32452  cvmlift2lem9  32461  cvmlift2lem12  32464  cvmlift2lem13  32465  cvmliftphtlem  32467  goel  32497  goelel3xp  32498  sat1el2xp  32529  fmla0xp  32533  prv1n  32581  msubco  32681  msubff1  32706  mvhf  32708  msubvrs  32710  fvtransport  33396  colinearex  33424  bj-idres  34350  icoreunrn  34528  relowlpssretop  34533  curf  34756  finixpnum  34763  poimirlem3  34781  poimirlem4  34782  poimirlem15  34793  poimirlem17  34795  poimirlem20  34798  poimirlem25  34803  poimirlem26  34804  poimirlem27  34805  heicant  34813  mblfinlem1  34815  mblfinlem2  34816  ftc1anc  34861  opropabco  34886  heiborlem5  34980  dvhelvbasei  38110  dvhopvadd  38115  dvhvaddcl  38117  dvhopvsca  38124  dvhvscacl  38125  dvhgrp  38129  dvhopclN  38135  dvhopaddN  38136  dvhopspN  38137  dib1dim2  38190  diblss  38192  diclspsn  38216  dih1dimatlem  38351  opelxpii  39001  hoicvr  42715  hoicvrrex  42723  ovnsubaddlem1  42737  ovnhoilem1  42768  ovnlecvr2  42777  opnvonmbllem1  42799  ovolval4lem2  42817  fnotaovb  43282  aovmpt4g  43285  rngccoALTV  44161  ringccoALTV  44224  rhmsubclem2  44260  rhmsubcALTVlem2  44278  rrx2plordisom  44612
  Copyright terms: Public domain W3C validator