Theorem opelxpi 4566

Description: Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opelxpi	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpi

Step	Hyp	Ref	Expression
1		opelxp 4564	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 132	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  ⟨cop 3525   × cxp 4532

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-pr 4126

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ral 2419  df-rex 2420  df-v 2683  df-un 3070  df-in 3072  df-ss 3079  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-opab 3985  df-xp 4540

This theorem is referenced by:  opelxpd  4567  opelvvg  4583  opelvv  4584  opbrop  4613  fliftrel  5686  fnotovb  5807  ovi3  5900  ovres  5903  fovrn  5906  fnovrn  5911  ovconst2  5915  oprab2co  6108  1stconst  6111  2ndconst  6112  f1od2  6125  brdifun  6449  ecopqsi  6477  brecop  6512  th3q  6527  xpcomco  6713  xpf1o  6731  xpmapenlem  6736  djulclr  6927  djurclr  6928  djulcl  6929  djurcl  6930  djuf1olem  6931  addpiord  7117  mulpiord  7118  enqeceq  7160  1nq  7167  addpipqqslem  7170  mulpipq  7173  mulpipqqs  7174  addclnq  7176  mulclnq  7177  recexnq  7191  ltexnqq  7209  prarloclemarch  7219  prarloclemarch2  7220  nnnq  7223  enq0breq  7237  enq0eceq  7238  nqnq0  7242  addnnnq0  7250  mulnnnq0  7251  addclnq0  7252  mulclnq0  7253  nqpnq0nq  7254  prarloclemlt  7294  prarloclemlo  7295  prarloclemcalc  7303  genpelxp  7312  nqprm  7343  ltexprlempr  7409  recexprlempr  7433  cauappcvgprlemcl  7454  cauappcvgprlemladd  7459  caucvgprlemcl  7477  caucvgprprlemcl  7505  enreceq  7537  addsrpr  7546  mulsrpr  7547  0r  7551  1sr  7552  m1r  7553  addclsr  7554  mulclsr  7555  prsrcl  7585  mappsrprg  7605  addcnsr  7635  mulcnsr  7636  addcnsrec  7643  mulcnsrec  7644  pitonnlem2  7648  pitonn  7649  pitore  7651  recnnre  7652  axaddcl  7665  axmulcl  7667  xrlenlt  7822  frecuzrdgg  10182  frecuzrdgsuctlem  10189  seq3val  10224  cnrecnv  10675  eucalgf  11725  eucalg  11729  qredeu  11767  qnumdenbi  11859  crth  11889  phimullem  11890  setscom  11988  setsslid  11998  txbas  12416  upxp  12430  uptx  12432  txlm  12437  cnmpt21  12449  txswaphmeolem  12478  txswaphmeo  12479  comet  12657  qtopbasss  12679  cnmetdval  12687  remetdval  12697  tgqioo  12705  dvcnp2cntop  12821  dvef  12845  djucllem  12996  pwle2  13182