fveq1i - Intuitionistic Logic Explorer

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

Theorem fveq1i 5495

Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)

**Hypothesis**
Ref	Expression
fveq1i.1

**Assertion**
Ref	Expression
fveq1i

**Proof of Theorem fveq1i**
Step	Hyp	Ref	Expression
1		fveq1i.1	. 2
2		fveq1 5493	. 2
3	1, 2	ax-mp 5	1

Colors of variables: wff set class

Syntax hints:

wceq 1348

cfv 5196

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152

This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-rex 2454 df-uni 3795 df-br 3988 df-iota 5158 df-fv 5204

This theorem is referenced by: fveq12i 5500 fvun2 5561 fvopab3ig 5568 fvsnun1 5691 fvsnun2 5692 fvpr1 5698 fvpr2 5699 fvpr1g 5700 fvpr2g 5701 fvtp1g 5702 fvtp2g 5703 fvtp3g 5704 fvtp2 5706 fvtp3 5707 ov 5970 ovigg 5971 ovg 5989 tfr2a 6298 tfrex 6345 frec0g 6374 freccllem 6379 frecsuclem 6383 caseinl 7065 caseinr 7066 ctssdccl 7085 addpiord 7267 mulpiord 7268 fseq1p1m1 10039 frec2uz0d 10344 frec2uzzd 10345 frec2uzsucd 10346 frecuzrdgrrn 10353 frec2uzrdg 10354 frecuzrdg0 10358 frecuzrdgsuc 10359 frecuzrdgg 10361 frecuzrdg0t 10367 frecuzrdgsuctlem 10368 0tonninf 10384 1tonninf 10385 inftonninf 10386 seq3val 10403 seqvalcd 10404 hashinfom 10701 hashennn 10703 hashfz1 10706 shftidt 10786 resqrexlemf1 10961 resqrexlemfp1 10962 cbvsum 11312 fisumss 11344 fsumadd 11358 isumclim3 11375 cbvprod 11510 fprodssdc 11542 ialgr0 11987 algrp1 11989 ennnfonelem0 12349 ennnfonelemp1 12350 ennnfonelemom 12352 ctinfomlemom 12371 nninfdclemp1 12394 ndxarg 12428 strslfv2d 12447 upxp 13027 cnmetdval 13284 remetdval 13294 reeflog 13539