opeq2d - Intuitionistic Logic Explorer

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

Theorem opeq2d 3911

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 3905	. 2
3	1, 2	syl 14	1

Colors of variables: wff set class

This proof depends on syntax axioms:

wi 4

wceq 1402

cop 3712

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-ext 2220

This proof depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-nf 1514 df-sb 1816 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-v 2823 df-un 3224 df-sn 3715 df-pr 3716 df-op 3718

This theorem is used by: tfr1onlemaccex 6623 tfrcllemaccex 6636 fundmen 7098 exmidapne 7632 recexnq 7763 suplocexprlemex 8095 elreal2 8203 frecuzrdgrrn 10866 frec2uzrdg 10867 frecuzrdgrcl 10868 frecuzrdgsuc 10872 frecuzrdgrclt 10873 frecuzrdgg 10874 frecuzrdgsuctlem 10881 seqeq2 10909 seqeq3 10910 iseqvalcbv 10917 seq3val 10918 seqvalcd 10919 s1val 11407 s1eq 11409 s1prc 11413 swrdlsw 11463 pfxpfx 11502 swrdccat 11529 swrdccat3blem 11533 swrdccat3b 11534 pfxccatin12d 11539 eucalgval 12857 ennnfonelemp1 13355 ennnfonelemnn0 13371 strsetsid 13443 ressvalsets 13476 strressid 13484 ressinbasd 13487 ressressg 13488 imasex 13685 imasival 13686 imasaddvallemg 13695 xpsfval 13728 prdsex 14279 prdsval 14280 xpsval 14308 mgpvalg 14327 mgpress 14337 ring1 14471 opprvalg 14483 sraval 14883 zlmval 15071 znval 15080 znval2 15082 psrval 15159 psrmulrg 15186 upgr1een 16570 uspgr1ewopdc 16690 usgr2v1e2w 16692 1loopgruspgr 16749 eupth2lem3lem3fi 16916 eupth2fi 16925