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 6770

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 6684	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5860	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6559	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 643	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6542	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6542	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ^◡ccnv 5661 Fun wfun 6531 ⟶wf 6533 –1-1→wf1 6534

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-ext 2741

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-sb 2098 df-clab 2748 df-cleq 2761 df-clel 2844 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-br 5114 df-opab 5178 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542

This theorem is referenced by: f1oeq1 6809 f1eq123d 6813 fo00 6858 f1prex 7283 f1iun 7940 tposf12 8246 oacomf1olem 8548 f1dom4g 8961 f1dom3g 8963 f1domg 8967 dom3d 8990 domtr 9003 0domg 9091 domssex2 9124 marypha1lem 9392 fseqenlem1 10007 dfac12lem2 10127 dfac12lem3 10128 ackbij2 10224 fin23lem28 10323 fin23lem32 10327 fin23lem34 10329 fin23lem35 10330 fin23lem41 10335 iundom2g 10523 pwfseqlem5 10647 hashf1lem1 14491 hashf1lem2 14492 hashf1 14493 4sqlem11 17014 injsubmefmnd 18955 conjsubgen 19320 sylow1lem2 19668 sylow2blem1 19689 hauspwpwf1 24112 oldfib 28535 istrkg2ld 28694 axlowdim 29251 sizusglecusg 29753 specval 32190 aciunf1lem 32947 zrhchr 34308 qqhre 34354 vonf1oonf1 35496 hashnexinj 42784 eldioph2lem2 43383 meadjiunlem 47070 fcoresf1b 47695 fundcmpsurbijinjpreimafv 48044 fundcmpsurinjpreimafv 48045 fundcmpsurinjimaid 48048 f1sn2g 49513 f102g 49514