opelxpd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > opelxpd		Structured version Visualization version GIF version

Theorem opelxpd 5711

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2099 ⟨cop 4630 × cxp 5670

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5293 ax-nul 5300 ax-pr 5423

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3472 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-opab 5205 df-xp 5678

This theorem is referenced by: otel3xp 5718 opabssxpd 5719 relssdmrn 6266 fpr2g 7217 fliftrel 7310 elovimad 7462 el2xptp0 8034 oprab2co 8096 1stconst 8099 2ndconst 8100 curry2 8106 fsplitfpar 8117 offsplitfpar 8118 fnwelem 8130 xpf1o 9157 xpmapenlem 9162 unxpdomlem3 9270 fseqenlem1 10041 fseqenlem2 10042 iundom2g 10557 ordpipq 10959 addpqf 10961 mulpqf 10963 recmulnq 10981 ltexnq 10992 axmulf 11163 cnrecnv 15138 ruclem1 16201 eucalgf 16547 qredeu 16622 crth 16740 phimullem 16741 prmreclem3 16880 setsstruct2 17136 imasaddflem 17505 xpsaddlem 17548 xpsvsca 17552 xpsle 17554 comffval 17672 oppccofval 17690 isoval 17741 brcic 17774 funcf2 17847 idfu2nd 17856 resf2nd 17874 wunfunc 17880 wunfuncOLD 17881 homaval 18013 setcco 18065 catcco 18087 estrcco 18113 xpcco 18167 xpchom2 18170 xpcco2 18171 xpccatid 18172 prfcl 18187 prf1st 18188 prf2nd 18189 evlf2 18203 curf1cl 18213 curf2cl 18216 curfcl 18217 uncf1 18221 uncf2 18222 uncfcurf 18224 diag11 18228 diag12 18229 diag2 18230 curf2ndf 18232 hof2fval 18240 yonedalem21 18258 yonedalem22 18263 yonedalem3b 18264 yonffthlem 18267 latcl2 18421 xpsmnd0 18728 xpsinv 19009 xpsgrpsub 19010 lsmhash 19653 frgpuplem 19720 xpsring1d 20262 rngqiprngimf 21180 pzriprnglem4 21403 pzriprnglem5 21404 pzriprnglem8 21407 pzriprnglem12 21411 mdetrlin 22497 mdetrsca 22498 txcls 23501 txcnp 23517 txcnmpt 23521 txdis1cn 23532 txlly 23533 txnlly 23534 txlm 23545 lmcn2 23546 txkgen 23549 xkococnlem 23556 txhmeo 23700 ptuncnv 23704 txflf 23903 flfcnp2 23904 tmdcn2 23986 qustgplem 24018 tsmsadd 24044 imasdsf1olem 24272 xpsdsval 24280 comet 24415 metustid 24456 metustexhalf 24458 metuel2 24467 tngnm 24561 cnheiborlem 24873 bcthlem5 25249 ovollb2lem 25410 ovolctb 25412 ovoliunlem2 25425 ovolshftlem1 25431 ovolscalem1 25435 ovolicc1 25438 ioombl1lem1 25480 dyadf 25513 itg1addlem4 25621 itg1addlem4OLD 25622 limccnp2 25814 dvaddbr 25861 dvmulbr 25862 dvmulbrOLD 25863 dvcobr 25870 dvcobrOLD 25871 lhop1lem 25939 cxpcn3 26676 mpodvdsmulf1o 27119 dvdsmulf1o 27121 addsqnreup 27369 addsval 27872 mulsval 28002 tgjustc1 28272 tgjustc2 28273 tgelrnln 28427 numclwwlk1lem2f 30158 ofresid 32421 fsuppcurry1 32501 fsuppcurry2 32502 gsumpart 32763 erlbrd 32971 rlocaddval 32976 rlocmulval 32977 rloccring 32978 rloc0g 32979 rloc1r 32980 rlocf1 32981 fracerl 32986 fracfld 32988 zringfrac 32990 prsdm 33509 prsrn 33510 esum2dlem 33705 hgt750lemb 34282 cvmlift2lem10 34916 goelel3xp 34952 sat1el2xp 34983 fmla0xp 34987 prv1n 35035 pprodss4v 35474 poimirlem3 37090 poimirlem4 37091 poimirlem17 37104 poimirlem20 37107 mblfinlem2 37125 aks6d1c3 41588 aks6d1c7lem1 41646 f1o2d2 41718 projf1o 44564 ovolval4lem1 46031 ovolval5lem2 46035

W3C validator

	
		OSZAR »