Theorem opelxpd 5628

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

Syntax hints:   → wi 4   ∈ wcel 2107  ⟨cop 4568   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5138  df-xp 5596

This theorem is referenced by:  otel3xp  5634  opabssxpd  5635  fpr2g  7096  fliftrel  7188  elovimad  7332  el2xptp0  7887  oprab2co  7946  1stconst  7949  2ndconst  7950  curry2  7956  fsplitfpar  7968  offsplitfpar  7969  fnwelem  7981  xpf1o  8935  xpmapenlem  8940  unxpdomlem3  9038  fseqenlem1  9789  fseqenlem2  9790  iundom2g  10305  ordpipq  10707  addpqf  10709  mulpqf  10711  recmulnq  10729  ltexnq  10740  axmulf  10911  cnrecnv  14885  ruclem1  15949  eucalgf  16297  qredeu  16372  crth  16488  phimullem  16489  prmreclem3  16628  setsstruct2  16884  imasaddflem  17250  xpsaddlem  17293  xpsvsca  17297  xpsle  17299  comffval  17417  oppccofval  17435  isoval  17486  brcic  17519  funcf2  17592  idfu2nd  17601  resf2nd  17619  wunfunc  17623  wunfuncOLD  17624  homaval  17755  setcco  17807  catcco  17829  estrcco  17855  xpcco  17909  xpchom2  17912  xpcco2  17913  xpccatid  17914  prfcl  17929  prf1st  17930  prf2nd  17931  evlf2  17945  curf1cl  17955  curf2cl  17958  curfcl  17959  uncf1  17963  uncf2  17964  uncfcurf  17966  diag11  17970  diag12  17971  diag2  17972  curf2ndf  17974  hof2fval  17982  yonedalem21  18000  yonedalem22  18005  yonedalem3b  18006  yonffthlem  18009  latcl2  18163  lsmhash  19320  frgpuplem  19387  mdetrlin  21760  mdetrsca  21761  txcls  22764  txcnp  22780  txcnmpt  22784  txdis1cn  22795  txlly  22796  txnlly  22797  txlm  22808  lmcn2  22809  txkgen  22812  xkococnlem  22819  txhmeo  22963  ptuncnv  22967  txflf  23166  flfcnp2  23167  tmdcn2  23249  qustgplem  23281  tsmsadd  23307  imasdsf1olem  23535  xpsdsval  23543  comet  23678  metustid  23719  metustexhalf  23721  metuel2  23730  tngnm  23824  cnheiborlem  24126  bcthlem5  24501  ovollb2lem  24661  ovolctb  24663  ovoliunlem2  24676  ovolshftlem1  24682  ovolscalem1  24686  ovolicc1  24689  ioombl1lem1  24731  dyadf  24764  itg1addlem4  24872  itg1addlem4OLD  24873  limccnp2  25065  dvaddbr  25111  dvmulbr  25112  dvcobr  25119  lhop1lem  25186  cxpcn3  25910  dvdsmulf1o  26352  addsqnreup  26600  tgjustc1  26845  tgjustc2  26846  tgelrnln  27000  numclwwlk1lem2f  28728  ofresid  30988  fsuppcurry1  31069  fsuppcurry2  31070  gsumpart  31324  prsdm  31873  prsrn  31874  esum2dlem  32069  hgt750lemb  32645  cvmlift2lem10  33283  goelel3xp  33319  sat1el2xp  33350  fmla0xp  33354  prv1n  33402  addsval  34135  pprodss4v  34195  poimirlem3  35789  poimirlem4  35790  poimirlem17  35803  poimirlem20  35806  mblfinlem2  35824  projf1o  42743  ovolval4lem1  44194  ovolval5lem2  44198