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 6624 tfrcllemaccex 6637 fundmen 7100 exmidapne 7632 recexnq 7763 suplocexprlemex 8095 elreal2 8203 frecuzrdgrrn 10865 frec2uzrdg 10866 frecuzrdgrcl 10867 frecuzrdgsuc 10871 frecuzrdgrclt 10872 frecuzrdgg 10873 frecuzrdgsuctlem 10880 seqeq2 10908 seqeq3 10909 iseqvalcbv 10916 seq3val 10917 seqvalcd 10918 s1val 11406 s1eq 11408 s1prc 11412 swrdlsw 11462 pfxpfx 11501 swrdccat 11528 swrdccat3blem 11532 swrdccat3b 11533 pfxccatin12d 11538 eucalgval 12856 ennnfonelemp1 13354 ennnfonelemnn0 13370 strsetsid 13442 ressvalsets 13475 strressid 13483 ressinbasd 13486 ressressg 13487 imasex 13684 imasival 13685 imasaddvallemg 13694 xpsfval 13727 prdsex 14278 prdsval 14279 xpsval 14307 mgpvalg 14326 mgpress 14336 ring1 14470 opprvalg 14482 sraval 14882 zlmval 15070 znval 15079 znval2 15081 psrval 15160 psrmulrg 15195 upgr1een 16587 uspgr1ewopdc 16707 usgr2v1e2w 16709 1loopgruspgr 16766 eupth2lem3lem3fi 16933 eupth2fi 16942