opeq2d - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > opeq2d		Unicode version

Theorem opeq2d 3874

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)

**Hypothesis**
Ref	Expression
opeq1d.1

**Assertion**
Ref	Expression
opeq2d

**Proof of Theorem opeq2d**
Step	Hyp	Ref	Expression
1		opeq1d.1	. 2
2		opeq2 3868	. 2
3	1, 2	syl 14	1

Colors of variables: wff set class

Syntax hints:

wi 4

wceq 1398

cop 3676

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-ext 2213

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-nf 1510 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-v 2805 df-un 3205 df-sn 3679 df-pr 3680 df-op 3682

This theorem is referenced by: tfr1onlemaccex 6557 tfrcllemaccex 6570 fundmen 7024 exmidapne 7539 recexnq 7670 suplocexprlemex 8002 elreal2 8110 frecuzrdgrrn 10733 frec2uzrdg 10734 frecuzrdgrcl 10735 frecuzrdgsuc 10739 frecuzrdgrclt 10740 frecuzrdgg 10741 frecuzrdgsuctlem 10748 seqeq2 10776 seqeq3 10777 iseqvalcbv 10784 seq3val 10785 seqvalcd 10786 s1val 11260 s1eq 11262 s1prc 11266 swrdlsw 11316 pfxpfx 11355 swrdccat 11382 swrdccat3blem 11386 swrdccat3b 11387 pfxccatin12d 11392 eucalgval 12706 ennnfonelemp1 13107 ennnfonelemnn0 13123 strsetsid 13195 ressvalsets 13227 strressid 13234 ressinbasd 13237 ressressg 13238 prdsex 13432 prdsval 13436 imasex 13468 imasival 13469 imasaddvallemg 13478 xpsfval 13511 xpsval 13515 mgpvalg 14017 mgpress 14025 ring1 14153 opprvalg 14163 sraval 14533 zlmval 14723 znval 14732 znval2 14734 psrval 14762 upgr1een 16065 uspgr1ewopdc 16185 usgr2v1e2w 16187 1loopgruspgr 16244 eupth2lem3lem3fi 16411 eupth2fi 16420