Theorem opelxpd 5701

Description: Ordered pair membership in a Cartesian product, deduction form. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypotheses

Ref	Expression
opelxpd.1	⊢ (𝜑 → 𝐴 ∈ 𝐶)
opelxpd.2	⊢ (𝜑 → 𝐵 ∈ 𝐷)

Assertion

Ref	Expression
opelxpd	⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpd

Step	Hyp	Ref	Expression
1		opelxpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
2		opelxpd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐷)
3		opelxpi 5699	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∈ wcel 2149  ⟨cop 4598   × cxp 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5176  df-xp 5668

This theorem is referenced by:  otel3xp  5708  opabssxpd  5709  relssdmrn  6271  fpr2g  7210  fliftrel  7307  elovimad  7461  el2xptp0  8033  oprab2co  8092  1stconst  8095  2ndconst  8096  curry2  8102  fsplitfpar  8113  offsplitfpar  8114  mpof1o2d  8121  fnwelem  8127  xpf1o  9127  xpmapenlem  9132  unxpdomlem3  9218  fseqenlem1  10008  fseqenlem2  10009  iundom2g  10524  ordpipq  10927  addpqf  10929  mulpqf  10931  recmulnq  10949  ltexnq  10960  axmulf  11131  cnrecnv  15216  ruclem1  16287  eucalgf  16641  qredeu  16716  crth  16837  phimullem  16838  prmreclem3  16978  setsstruct2  17234  imasaddflem  17584  xpsaddlem  17627  xpsvsca  17631  xpsle  17633  comffval  17755  oppccofval  17772  isoval  17822  brcic  17855  funcf2  17925  idfu2nd  17934  resf2nd  17952  wunfunc  17958  homaval  18088  setcco  18140  catcco  18162  estrcco  18186  xpcco  18239  xpchom2  18242  xpcco2  18243  xpccatid  18244  prfcl  18259  prf1st  18260  prf2nd  18261  evlf2  18274  curf1cl  18284  curf2cl  18287  curfcl  18288  uncf1  18292  uncf2  18293  uncfcurf  18295  diag11  18299  diag12  18300  diag2  18301  curf2ndf  18303  hof2fval  18311  yonedalem21  18329  yonedalem22  18334  yonedalem3b  18335  yonffthlem  18338  latcl2  18492  xpsmnd0  18836  xpsinv  19126  xpsgrpsub  19127  lsmhash  19775  frgpuplem  19842  xpsring1d  20415  rngqiprngimf  21408  pzriprnglem4  21603  pzriprnglem5  21604  pzriprnglem8  21607  pzriprnglem12  21611  mdetrlin  22728  mdetrsca  22729  txcls  23730  txcnp  23746  txcnmpt  23750  txdis1cn  23761  txlly  23762  txnlly  23763  txlm  23774  lmcn2  23775  txkgen  23778  xkococnlem  23785  txhmeo  23929  ptuncnv  23933  txflf  24132  flfcnp2  24133  tmdcn2  24215  qustgplem  24247  tsmsadd  24273  imasdsf1olem  24499  xpsdsval  24507  comet  24639  metustid  24680  metustexhalf  24682  metuel2  24691  tngnm  24777  cnheiborlem  25082  bcthlem5  25456  ovollb2lem  25616  ovolctb  25618  ovoliunlem2  25631  ovolshftlem1  25637  ovolscalem1  25641  ovolicc1  25644  ioombl1lem1  25686  dyadf  25719  itg1addlem4  25827  limccnp2  26020  dvaddbr  26066  dvmulbr  26067  dvcobr  26074  lhop1lem  26141  cxpcn3  26879  mpodvdsmulf1o  27324  dvdsmulf1o  27326  addsqnreup  27573  addsval  28121  mulsval  28268  tgjustc1  28710  tgjustc2  28711  tgelrnln  28865  tgelrnpln  29016  numclwwlk1lem2f  30647  ofresid  32928  fsuppcurry1  33010  fsuppcurry2  33011  gsumpart  33324  gsumwrd2dccatlem  33338  gsumwrd2dccat  33339  elrgspnsubrunlem2  33509  erlbrd  33524  erld2  33527  rlocaddval  33530  rlocmulval  33531  rloccring  33532  rloc0g  33533  rloc1r  33534  rlocf1  33535  rlocinvunit  33536  rlocisunit  33537  fracerl  33570  fracfld  33572  zringfrac  33789  prsdm  34249  prsrn  34250  esum2dlem  34427  hgt750lemb  34988  cvmlift2lem10  35737  goelel3xp  35773  sat1el2xp  35804  fmla0xp  35808  prv1n  35856  pprodss4v  36307  nmulprop  36615  poimirlem3  38197  poimirlem4  38198  poimirlem17  38211  poimirlem20  38214  mblfinlem2  38232  aks6d1c3  42815  aks6d1c7lem1  42872  projf1o  45841  hoicvr  47189  ovolval4lem1  47290  ovolval5lem2  47294  gpgiedgdmellem  48735  gpgvtx0  48742  gpgvtx1  48743  gpg3kgrtriex  48778  gpgprismgr4cycllem3  48786  gpgprismgr4cycllem9  48792  tposidres  49584  oppf1st2nd  49829  imaid  49852  xpcfuccocl  49955  swapf1  49970  swapf2val  49971  swapf2  49972  cofuswapf1  49992  cofuswapf2  49993  lanfval  50311  ranfval  50312