f1eq1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f1eq1		Structured version Visualization version GIF version

Theorem f1eq1 6257

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)

**Assertion**
Ref	Expression
f1eq1	⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

**Proof of Theorem f1eq1**
Step	Hyp	Ref	Expression
1		feq1 6187	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5451	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6071	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 749	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6054	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6054	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 303	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1632 ^◡ccnv 5265 Fun wfun 6043 ⟶wf 6045 –1-1→wf1 6046

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-br 4805 df-opab 4865 df-rel 5273 df-cnv 5274 df-co 5275 df-dm 5276 df-rn 5277 df-fun 6051 df-fn 6052 df-f 6053 df-f1 6054

This theorem is referenced by: f1oeq1 6288 f1eq123d 6292 fo00 6333 f1prex 6702 fun11iun 7291 tposf12 7546 oacomf1olem 7813 f1dom2g 8139 f1domg 8141 dom3d 8163 domtr 8174 domssex2 8285 1sdom 8328 marypha1lem 8504 fseqenlem1 9037 dfac12lem2 9158 dfac12lem3 9159 ackbij2 9257 fin23lem28 9354 fin23lem32 9358 fin23lem34 9360 fin23lem35 9361 fin23lem41 9366 iundom2g 9554 pwfseqlem5 9677 hashf1lem1 13431 hashf1lem2 13432 hashf1 13433 4sqlem11 15861 conjsubgen 17894 sylow1lem2 18214 sylow2blem1 18235 hauspwpwf1 21992 istrkg2ld 25558 axlowdim 26040 sizusglecusg 26569 specval 29066 aciunf1lem 29771 zrhchr 30329 qqhre 30373 eldioph2lem2 37826 meadjiunlem 41185