Theorem opelxpd 5593

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

Syntax hints:   → wi 4   ∈ wcel 2114  ⟨cop 4573   × cxp 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5129  df-xp 5561

This theorem is referenced by:  otel3xp  5599  opabssxpd  5789  fpr2g  6974  fliftrel  7061  elovimad  7204  el2xptp0  7736  oprab2co  7792  1stconst  7795  2ndconst  7796  curry2  7802  fsplitfpar  7814  offsplitfpar  7815  fnwelem  7825  xpf1o  8679  xpmapenlem  8684  unxpdomlem3  8724  fseqenlem1  9450  fseqenlem2  9451  iundom2g  9962  ordpipq  10364  addpqf  10366  mulpqf  10368  recmulnq  10386  ltexnq  10397  axmulf  10568  cnrecnv  14524  ruclem1  15584  eucalgf  15927  qredeu  16002  crth  16115  phimullem  16116  prmreclem3  16254  setsstruct2  16521  imasaddflem  16803  xpsaddlem  16846  xpsvsca  16850  xpsle  16852  comffval  16969  oppccofval  16986  isoval  17035  brcic  17068  funcf2  17138  idfu2nd  17147  resf2nd  17165  wunfunc  17169  homaval  17291  setcco  17343  catcco  17361  estrcco  17380  xpcco  17433  xpchom2  17436  xpcco2  17437  xpccatid  17438  prfcl  17453  prf1st  17454  prf2nd  17455  evlf2  17468  curf1cl  17478  curf2cl  17481  curfcl  17482  uncf1  17486  uncf2  17487  uncfcurf  17489  diag11  17493  diag12  17494  diag2  17495  curf2ndf  17497  hof2fval  17505  yonedalem21  17523  yonedalem22  17528  yonedalem3b  17529  yonffthlem  17532  latcl2  17658  lsmhash  18831  frgpuplem  18898  mdetrlin  21211  mdetrsca  21212  txcls  22212  txcnp  22228  txcnmpt  22232  txdis1cn  22243  txlly  22244  txnlly  22245  txlm  22256  lmcn2  22257  txkgen  22260  xkococnlem  22267  txhmeo  22411  ptuncnv  22415  txflf  22614  flfcnp2  22615  tmdcn2  22697  qustgplem  22729  tsmsadd  22755  imasdsf1olem  22983  xpsdsval  22991  comet  23123  metustid  23164  metustexhalf  23166  metuel2  23175  tngnm  23260  cnheiborlem  23558  bcthlem5  23931  ovollb2lem  24089  ovolctb  24091  ovoliunlem2  24104  ovolshftlem1  24110  ovolscalem1  24114  ovolicc1  24117  ioombl1lem1  24159  dyadf  24192  itg1addlem4  24300  limccnp2  24490  dvaddbr  24535  dvmulbr  24536  dvcobr  24543  lhop1lem  24610  cxpcn3  25329  dvdsmulf1o  25771  addsqnreup  26019  tgjustc1  26261  tgjustc2  26262  tgelrnln  26416  numclwwlk1lem2f  28134  ofresid  30389  fsuppcurry1  30461  fsuppcurry2  30462  prsdm  31157  prsrn  31158  esum2dlem  31351  hgt750lemb  31927  cvmlift2lem10  32559  goelel3xp  32595  sat1el2xp  32626  fmla0xp  32630  prv1n  32678  pprodss4v  33345  mblfinlem2  34945  projf1o  41508  ovolval4lem1  42980  ovolval5lem2  42984