fveq1i - Intuitionistic Logic Explorer

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

Theorem fveq1i 5497

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 5495	. 2
3	1, 2	ax-mp 5	1

Colors of variables: wff set class

Syntax hints:

wceq 1348

cfv 5198

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 3797 df-br 3990 df-iota 5160 df-fv 5206

This theorem is referenced by: fveq12i 5502 fvun2 5563 fvopab3ig 5570 fvsnun1 5693 fvsnun2 5694 fvpr1 5700 fvpr2 5701 fvpr1g 5702 fvpr2g 5703 fvtp1g 5704 fvtp2g 5705 fvtp3g 5706 fvtp2 5708 fvtp3 5709 ov 5972 ovigg 5973 ovg 5991 tfr2a 6300 tfrex 6347 frec0g 6376 freccllem 6381 frecsuclem 6385 caseinl 7068 caseinr 7069 ctssdccl 7088 addpiord 7278 mulpiord 7279 fseq1p1m1 10050 frec2uz0d 10355 frec2uzzd 10356 frec2uzsucd 10357 frecuzrdgrrn 10364 frec2uzrdg 10365 frecuzrdg0 10369 frecuzrdgsuc 10370 frecuzrdgg 10372 frecuzrdg0t 10378 frecuzrdgsuctlem 10379 0tonninf 10395 1tonninf 10396 inftonninf 10397 seq3val 10414 seqvalcd 10415 hashinfom 10712 hashennn 10714 hashfz1 10717 shftidt 10797 resqrexlemf1 10972 resqrexlemfp1 10973 cbvsum 11323 fisumss 11355 fsumadd 11369 isumclim3 11386 cbvprod 11521 fprodssdc 11553 ialgr0 11998 algrp1 12000 ennnfonelem0 12360 ennnfonelemp1 12361 ennnfonelemom 12363 ctinfomlemom 12382 nninfdclemp1 12405 ndxarg 12439 strslfv2d 12458 upxp 13066 cnmetdval 13323 remetdval 13333 reeflog 13578