Theorem opelxpi 4529

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 4527	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 132	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1461  ⟨cop 3494   × cxp 4495

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-opab 3948  df-xp 4503

This theorem is referenced by:  opelxpd  4530  opelvvg  4546  opelvv  4547  opbrop  4576  fliftrel  5645  fnotovb  5766  ovi3  5859  ovres  5862  fovrn  5865  fnovrn  5870  ovconst2  5874  oprab2co  6066  1stconst  6069  2ndconst  6070  f1od2  6083  brdifun  6407  ecopqsi  6435  brecop  6470  th3q  6485  xpcomco  6670  xpf1o  6688  xpmapenlem  6693  djulclr  6883  djurclr  6884  djulcl  6885  djurcl  6886  djuf1olem  6887  addpiord  7065  mulpiord  7066  enqeceq  7108  1nq  7115  addpipqqslem  7118  mulpipq  7121  mulpipqqs  7122  addclnq  7124  mulclnq  7125  recexnq  7139  ltexnqq  7157  prarloclemarch  7167  prarloclemarch2  7168  nnnq  7171  enq0breq  7185  enq0eceq  7186  nqnq0  7190  addnnnq0  7198  mulnnnq0  7199  addclnq0  7200  mulclnq0  7201  nqpnq0nq  7202  prarloclemlt  7242  prarloclemlo  7243  prarloclemcalc  7251  genpelxp  7260  nqprm  7291  ltexprlempr  7357  recexprlempr  7381  cauappcvgprlemcl  7402  cauappcvgprlemladd  7407  caucvgprlemcl  7425  caucvgprprlemcl  7453  enreceq  7472  addsrpr  7481  mulsrpr  7482  0r  7486  1sr  7487  m1r  7488  addclsr  7489  mulclsr  7490  prsrcl  7519  addcnsr  7562  mulcnsr  7563  addcnsrec  7570  mulcnsrec  7571  pitonnlem2  7575  pitonn  7576  pitore  7578  recnnre  7579  axaddcl  7592  axmulcl  7594  xrlenlt  7746  frecuzrdgg  10075  frecuzrdgsuctlem  10082  seq3val  10117  cnrecnv  10568  eucalgf  11575  eucalg  11579  qredeu  11617  qnumdenbi  11708  crth  11738  phimullem  11739  setscom  11835  setsslid  11845  txbas  12262  upxp  12276  uptx  12278  txlm  12283  cnmpt21  12295  comet  12481  qtopbasss  12503  cnmetdval  12511  remetdval  12518  tgqioo  12526  dvcnp2cntop  12611  djucllem  12686  pwle2  12872