![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fveq1 | GIF version |
Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.) |
Ref | Expression |
---|---|
fveq1 | ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq 3853 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥)) | |
2 | 1 | iotabidv 5014 | . 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥)) |
3 | df-fv 5036 | . 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥) | |
4 | df-fv 5036 | . 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥) | |
5 | 2, 3, 4 | 3eqtr4g 2146 | 1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1290 class class class wbr 3851 ℩cio 4991 ‘cfv 5028 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-rex 2366 df-uni 3660 df-br 3852 df-iota 4993 df-fv 5036 |
This theorem is referenced by: fveq1i 5319 fveq1d 5320 fvmptdf 5403 fvmptdv2 5405 isoeq1 5594 oveq 5672 offval 5877 ofrfval 5878 offval3 5919 smoeq 6069 recseq 6085 tfr0dm 6101 tfrlemiex 6110 tfr1onlemex 6126 tfr1onlemaccex 6127 tfrcllemsucaccv 6133 tfrcllembxssdm 6135 tfrcllemex 6139 tfrcllemaccex 6140 tfrcllemres 6141 rdgeq1 6150 rdgivallem 6160 rdgon 6165 rdg0 6166 frec0g 6176 freccllem 6181 frecfcllem 6183 frecsuclem 6185 frecsuc 6186 mapsncnv 6466 elixp2 6473 elixpsn 6506 mapsnen 6582 mapxpen 6618 ac6sfi 6668 updjud 6827 enomnilem 6855 finomni 6857 exmidomni 6859 fodjuomnilemres 6864 infnninf 6866 nnnninf 6867 1fv 9611 iseqeq3 9921 iseqf1olemjpcl 9985 iseqf1olemqpcl 9986 iseqf1olemfvp 9987 seq3f1olemqsum 9990 seq3f1olemstep 9991 seq3f1olemp 9992 shftvalg 10331 shftval4g 10332 clim 10730 isummo 10834 fisum 10839 strnfvnd 11575 elcncf 11902 0nninf 12165 nninff 12166 nnsf 12167 peano4nninf 12168 peano3nninf 12169 nninfalllemn 12170 nninfalllem1 12171 nninfself 12177 nninfsellemeq 12178 nninfsellemeqinf 12180 |
Copyright terms: Public domain | W3C validator |