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 6619 tfrcllemaccex 6632 fundmen 7094 exmidapne 7627 recexnq 7758 suplocexprlemex 8090 elreal2 8198 frecuzrdgrrn 10860 frec2uzrdg 10861 frecuzrdgrcl 10862 frecuzrdgsuc 10866 frecuzrdgrclt 10867 frecuzrdgg 10868 frecuzrdgsuctlem 10875 seqeq2 10903 seqeq3 10904 iseqvalcbv 10911 seq3val 10912 seqvalcd 10913 s1val 11401 s1eq 11403 s1prc 11407 swrdlsw 11457 pfxpfx 11496 swrdccat 11523 swrdccat3blem 11527 swrdccat3b 11528 pfxccatin12d 11533 eucalgval 12851 ennnfonelemp1 13349 ennnfonelemnn0 13365 strsetsid 13437 ressvalsets 13470 strressid 13478 ressinbasd 13481 ressressg 13482 imasex 13679 imasival 13680 imasaddvallemg 13689 xpsfval 13722 prdsex 14256 prdsval 14257 xpsval 14285 mgpvalg 14304 mgpress 14314 ring1 14448 opprvalg 14458 sraval 14858 zlmval 15046 znval 15055 znval2 15057 psrval 15134 psrmulrg 15158 upgr1een 16531 uspgr1ewopdc 16651 usgr2v1e2w 16653 1loopgruspgr 16710 eupth2lem3lem3fi 16877 eupth2fi 16886