fveq1i - Intuitionistic Logic Explorer

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

Theorem fveq1i 5486

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

Colors of variables: wff set class

Syntax hints:

wceq 1343

cfv 5187

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 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-ext 2147

This theorem depends on definitions: df-bi 116 df-tru 1346 df-nf 1449 df-sb 1751 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2296 df-rex 2449 df-uni 3789 df-br 3982 df-iota 5152 df-fv 5195

This theorem is referenced by: fveq12i 5491 fvun2 5552 fvopab3ig 5559 fvsnun1 5681 fvsnun2 5682 fvpr1 5688 fvpr2 5689 fvpr1g 5690 fvpr2g 5691 fvtp1g 5692 fvtp2g 5693 fvtp3g 5694 fvtp2 5696 fvtp3 5697 ov 5957 ovigg 5958 ovg 5976 tfr2a 6285 tfrex 6332 frec0g 6361 freccllem 6366 frecsuclem 6370 caseinl 7052 caseinr 7053 ctssdccl 7072 addpiord 7253 mulpiord 7254 fseq1p1m1 10025 frec2uz0d 10330 frec2uzzd 10331 frec2uzsucd 10332 frecuzrdgrrn 10339 frec2uzrdg 10340 frecuzrdg0 10344 frecuzrdgsuc 10345 frecuzrdgg 10347 frecuzrdg0t 10353 frecuzrdgsuctlem 10354 0tonninf 10370 1tonninf 10371 inftonninf 10372 seq3val 10389 seqvalcd 10390 hashinfom 10687 hashennn 10689 hashfz1 10692 shftidt 10771 resqrexlemf1 10946 resqrexlemfp1 10947 cbvsum 11297 fisumss 11329 fsumadd 11343 isumclim3 11360 cbvprod 11495 fprodssdc 11527 ialgr0 11972 algrp1 11974 ennnfonelem0 12334 ennnfonelemp1 12335 ennnfonelemom 12337 ctinfomlemom 12356 nninfdclemp1 12379 ndxarg 12413 strslfv2d 12432 upxp 12872 cnmetdval 13129 remetdval 13139 reeflog 13384