Theorem opelxpd 5658

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

Syntax hints:   → wi 4   ∈ wcel 2109  ⟨cop 4583   × cxp 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-opab 5155  df-xp 5625

This theorem is referenced by:  otel3xp  5665  opabssxpd  5666  relssdmrn  6217  fpr2g  7147  fliftrel  7245  elovimad  7399  el2xptp0  7971  oprab2co  8030  1stconst  8033  2ndconst  8034  curry2  8040  fsplitfpar  8051  offsplitfpar  8052  fnwelem  8064  xpf1o  9056  xpmapenlem  9061  unxpdomlem3  9147  fseqenlem1  9918  fseqenlem2  9919  iundom2g  10434  ordpipq  10836  addpqf  10838  mulpqf  10840  recmulnq  10858  ltexnq  10869  axmulf  11040  cnrecnv  15072  ruclem1  16140  eucalgf  16494  qredeu  16569  crth  16689  phimullem  16690  prmreclem3  16830  setsstruct2  17085  imasaddflem  17434  xpsaddlem  17477  xpsvsca  17481  xpsle  17483  comffval  17605  oppccofval  17622  isoval  17672  brcic  17705  funcf2  17775  idfu2nd  17784  resf2nd  17802  wunfunc  17808  homaval  17938  setcco  17990  catcco  18012  estrcco  18036  xpcco  18089  xpchom2  18092  xpcco2  18093  xpccatid  18094  prfcl  18109  prf1st  18110  prf2nd  18111  evlf2  18124  curf1cl  18134  curf2cl  18137  curfcl  18138  uncf1  18142  uncf2  18143  uncfcurf  18145  diag11  18149  diag12  18150  diag2  18151  curf2ndf  18153  hof2fval  18161  yonedalem21  18179  yonedalem22  18184  yonedalem3b  18185  yonffthlem  18188  latcl2  18342  xpsmnd0  18652  xpsinv  18939  xpsgrpsub  18940  lsmhash  19584  frgpuplem  19651  xpsring1d  20218  rngqiprngimf  21204  pzriprnglem4  21391  pzriprnglem5  21392  pzriprnglem8  21395  pzriprnglem12  21399  mdetrlin  22487  mdetrsca  22488  txcls  23489  txcnp  23505  txcnmpt  23509  txdis1cn  23520  txlly  23521  txnlly  23522  txlm  23533  lmcn2  23534  txkgen  23537  xkococnlem  23544  txhmeo  23688  ptuncnv  23692  txflf  23891  flfcnp2  23892  tmdcn2  23974  qustgplem  24006  tsmsadd  24032  imasdsf1olem  24259  xpsdsval  24267  comet  24399  metustid  24440  metustexhalf  24442  metuel2  24451  tngnm  24537  cnheiborlem  24851  bcthlem5  25226  ovollb2lem  25387  ovolctb  25389  ovoliunlem2  25402  ovolshftlem1  25408  ovolscalem1  25412  ovolicc1  25415  ioombl1lem1  25457  dyadf  25490  itg1addlem4  25598  limccnp2  25791  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvcobr  25847  dvcobrOLD  25848  lhop1lem  25916  cxpcn3  26656  mpodvdsmulf1o  27102  dvdsmulf1o  27104  addsqnreup  27352  addsval  27876  mulsval  28019  tgjustc1  28424  tgjustc2  28425  tgelrnln  28579  numclwwlk1lem2f  30303  ofresid  32593  fsuppcurry1  32676  fsuppcurry2  32677  gsumpart  33019  gsumwrd2dccatlem  33028  gsumwrd2dccat  33029  elrgspnsubrunlem2  33197  erlbrd  33212  rlocaddval  33217  rlocmulval  33218  rloccring  33219  rloc0g  33220  rloc1r  33221  rlocf1  33222  fracerl  33254  fracfld  33256  zringfrac  33500  prsdm  33897  prsrn  33898  esum2dlem  34075  hgt750lemb  34640  cvmlift2lem10  35305  goelel3xp  35341  sat1el2xp  35372  fmla0xp  35376  prv1n  35424  pprodss4v  35878  poimirlem3  37623  poimirlem4  37624  poimirlem17  37637  poimirlem20  37640  mblfinlem2  37658  aks6d1c3  42116  aks6d1c7lem1  42173  f1o2d2  42226  projf1o  45195  ovolval4lem1  46650  ovolval5lem2  46654  gpgiedgdmellem  48050  gpgvtx0  48057  gpgvtx1  48058  gpg3kgrtriex  48093  gpgprismgr4cycllem3  48101  gpgprismgr4cycllem9  48107  tposidres  48890  oppf1st2nd  49136  imaid  49159  xpcfuccocl  49262  swapf1  49277  swapf2val  49278  swapf2  49279  cofuswapf1  49299  cofuswapf2  49300  lanfval  49618  ranfval  49619