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 6755

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 6669	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5845	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6543	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 641	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6526	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6526	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 316	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1560 ^◡ccnv 5646 Fun wfun 6515 ⟶wf 6517 –1-1→wf1 6518

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-ext 2734

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-sb 2091 df-clab 2741 df-cleq 2754 df-clel 2837 df-rab 3415 df-v 3456 df-dif 3907 df-un 3909 df-ss 3921 df-nul 4286 df-if 4481 df-sn 4583 df-pr 4585 df-op 4589 df-br 5101 df-opab 5163 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526

This theorem is referenced by: f1oeq1 6794 f1eq123d 6798 fo00 6843 f1prex 7268 f1iun 7925 tposf12 8231 oacomf1olem 8533 f1dom4g 8946 f1dom3g 8948 f1domg 8952 dom3d 8975 domtr 8988 0domg 9076 domssex2 9109 marypha1lem 9379 fseqenlem1 9980 dfac12lem2 10101 dfac12lem3 10102 ackbij2 10198 fin23lem28 10297 fin23lem32 10301 fin23lem34 10303 fin23lem35 10304 fin23lem41 10309 iundom2g 10497 pwfseqlem5 10621 hashf1lem1 14468 hashf1lem2 14469 hashf1 14470 4sqlem11 16991 injsubmefmnd 18931 conjsubgen 19291 sylow1lem2 19639 sylow2blem1 19660 hauspwpwf1 24044 oldfib 28467 istrkg2ld 28626 axlowdim 29159 sizusglecusg 29661 specval 32098 aciunf1lem 32861 zrhchr 34268 qqhre 34314 vonf1oonf1 35454 hashnexinj 42742 eldioph2lem2 43339 meadjiunlem 47036 fcoresf1b 47661 fundcmpsurbijinjpreimafv 48010 fundcmpsurinjpreimafv 48011 fundcmpsurinjimaid 48014 f1sn2g 49469 f102g 49470