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 6769

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 6683	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5859	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6558	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 643	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6541	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6541	. 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 1570 ^◡ccnv 5660 Fun wfun 6530 ⟶wf 6532 –1-1→wf1 6533

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-ext 2735

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-sb 2097 df-clab 2742 df-cleq 2755 df-clel 2838 df-rab 3417 df-v 3457 df-dif 3908 df-un 3910 df-ss 3922 df-nul 4287 df-if 4488 df-sn 4590 df-pr 4592 df-op 4596 df-br 5110 df-opab 5174 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541

This theorem is referenced by: f1oeq1 6808 f1eq123d 6812 fo00 6857 f1prex 7282 f1iun 7937 tposf12 8243 oacomf1olem 8545 f1dom4g 8958 f1dom3g 8960 f1domg 8964 dom3d 8987 domtr 9000 0domg 9088 domssex2 9121 marypha1lem 9389 fseqenlem1 10004 dfac12lem2 10124 dfac12lem3 10125 ackbij2 10221 fin23lem28 10319 fin23lem32 10323 fin23lem34 10325 fin23lem35 10326 fin23lem41 10331 iundom2g 10519 pwfseqlem5 10643 hashf1lem1 14488 hashf1lem2 14489 hashf1 14490 4sqlem11 17010 injsubmefmnd 18951 conjsubgen 19316 sylow1lem2 19664 sylow2blem1 19685 hauspwpwf1 24144 oldfib 28570 istrkg2ld 28729 axlowdim 29311 sizusglecusg 29813 specval 32250 aciunf1lem 33007 zrhchr 34364 qqhre 34410 vonf1oonf1 35598 hashnexinj 42895 eldioph2lem2 43492 meadjiunlem 47179 fcoresf1b 47807 fundcmpsurbijinjpreimafv 48156 fundcmpsurinjpreimafv 48157 fundcmpsurinjimaid 48160 f1sn2g 49629 f102g 49630