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 6430

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 6355	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5622	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6239	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 630	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6222	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6222	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 315	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1520 ^◡ccnv 5434 Fun wfun 6211 ⟶wf 6213 –1-1→wf1 6214

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-rab 3112 df-v 3434 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-sn 4467 df-pr 4469 df-op 4473 df-br 4957 df-opab 5019 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222

This theorem is referenced by: f1oeq1 6464 f1eq123d 6468 fo00 6510 f1prex 6896 fun11iun 7492 tposf12 7759 oacomf1olem 8031 f1dom2g 8365 f1domg 8367 dom3d 8389 domtr 8400 domssex2 8514 1sdom 8557 marypha1lem 8733 fseqenlem1 9285 dfac12lem2 9405 dfac12lem3 9406 ackbij2 9500 fin23lem28 9597 fin23lem32 9601 fin23lem34 9603 fin23lem35 9604 fin23lem41 9609 iundom2g 9797 pwfseqlem5 9920 hashf1lem1 13649 hashf1lem2 13650 hashf1 13651 4sqlem11 16108 conjsubgen 18120 sylow1lem2 18442 sylow2blem1 18463 hauspwpwf1 22267 istrkg2ld 25916 axlowdim 26418 sizusglecusg 26916 specval 29354 aciunf1lem 30070 zrhchr 30790 qqhre 30834 eldioph2lem2 38793 meadjiunlem 42243