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 6278

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 6204	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5464	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6090	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 624	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6073	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6073	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 305	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 = wceq 1652 ^◡ccnv 5276 Fun wfun 6062 ⟶wf 6064 –1-1→wf1 6065

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-rab 3064 df-v 3352 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-nul 4080 df-if 4244 df-sn 4335 df-pr 4337 df-op 4341 df-br 4810 df-opab 4872 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-fun 6070 df-fn 6071 df-f 6072 df-f1 6073

This theorem is referenced by: f1oeq1 6310 f1eq123d 6314 fo00 6355 f1prex 6731 fun11iun 7324 tposf12 7580 oacomf1olem 7849 f1dom2g 8178 f1domg 8180 dom3d 8202 domtr 8213 domssex2 8327 1sdom 8370 marypha1lem 8546 fseqenlem1 9098 dfac12lem2 9219 dfac12lem3 9220 ackbij2 9318 fin23lem28 9415 fin23lem32 9419 fin23lem34 9421 fin23lem35 9422 fin23lem41 9427 iundom2g 9615 pwfseqlem5 9738 hashf1lem1 13440 hashf1lem2 13441 hashf1 13442 4sqlem11 15940 conjsubgen 17959 sylow1lem2 18280 sylow2blem1 18301 hauspwpwf1 22070 istrkg2ld 25650 axlowdim 26132 sizusglecusg 26650 specval 29148 aciunf1lem 29847 zrhchr 30402 qqhre 30446 eldioph2lem2 37934 meadjiunlem 41251