Theorem opelxpd 5488

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 5487	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∈ wcel 2083  ⟨cop 4484   × cxp 5448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-opab 5031  df-xp 5456

This theorem is referenced by:  otel3xp  5494  opabssxpd  5682  fpr2g  6847  fliftrel  6931  elovimad  7070  el2xptp0  7599  oprab2co  7655  1stconst  7658  2ndconst  7659  curry2  7665  fnwelem  7685  xpf1o  8533  xpmapenlem  8538  unxpdomlem3  8577  fseqenlem1  9303  fseqenlem2  9304  iundom2g  9815  ordpipq  10217  addpqf  10219  mulpqf  10221  recmulnq  10239  ltexnq  10250  axmulf  10421  cnrecnv  14362  ruclem1  15421  eucalgf  15760  qredeu  15835  crth  15948  phimullem  15949  prmreclem3  16087  setsstruct2  16354  imasaddflem  16636  xpsaddlem  16679  xpsvsca  16683  xpsle  16685  comffval  16802  oppccofval  16819  isoval  16868  brcic  16901  funcf2  16971  idfu2nd  16980  resf2nd  16998  wunfunc  17002  homaval  17124  setcco  17176  catcco  17194  estrcco  17213  xpcco  17266  xpchom2  17269  xpcco2  17270  xpccatid  17271  prfcl  17286  prf1st  17287  prf2nd  17288  evlf2  17301  curf1cl  17311  curf2cl  17314  curfcl  17315  uncf1  17319  uncf2  17320  uncfcurf  17322  diag11  17326  diag12  17327  diag2  17328  curf2ndf  17330  hof2fval  17338  yonedalem21  17356  yonedalem22  17361  yonedalem3b  17362  yonffthlem  17365  latcl2  17491  lsmhash  18562  frgpuplem  18629  mdetrlin  20899  mdetrsca  20900  txcls  21900  txcnp  21916  txcnmpt  21920  txdis1cn  21931  txlly  21932  txnlly  21933  txlm  21944  lmcn2  21945  txkgen  21948  xkococnlem  21955  txhmeo  22099  ptuncnv  22103  txflf  22302  flfcnp2  22303  tmdcn2  22385  qustgplem  22416  tsmsadd  22442  imasdsf1olem  22670  xpsdsval  22678  comet  22810  metustid  22851  metustexhalf  22853  metuel2  22862  tngnm  22947  cnheiborlem  23245  bcthlem5  23618  ovollb2lem  23776  ovolctb  23778  ovoliunlem2  23791  ovolshftlem1  23797  ovolscalem1  23801  ovolicc1  23804  ioombl1lem1  23846  dyadf  23879  itg1addlem4  23987  limccnp2  24177  dvaddbr  24222  dvmulbr  24223  dvcobr  24230  lhop1lem  24297  cxpcn3  25014  dvdsmulf1o  25457  addsqnreup  25705  tgjustc1  25947  tgjustc2  25948  tgelrnln  26102  numclwwlk1lem2f  27822  ofresid  30075  fsuppcurry1  30145  fsuppcurry2  30146  prsdm  30770  prsrn  30771  esum2dlem  30964  hgt750lemb  31540  cvmlift2lem10  32169  goelel3xp  32205  sat1el2xp  32236  fmla0xp  32240  prv1n  32288  pprodss4v  32956  mblfinlem2  34482  projf1o  41020  ovolval4lem1  42495  ovolval5lem2  42499