Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > f1oeq123d | Structured version Visualization version GIF version |
Description: Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Ref | Expression |
---|---|
f1eq123d.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
f1eq123d.2 | ⊢ (𝜑 → 𝐴 = 𝐵) |
f1eq123d.3 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
f1oeq123d | ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1eq123d.1 | . . 3 ⊢ (𝜑 → 𝐹 = 𝐺) | |
2 | f1oeq1 6606 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶)) |
4 | f1eq123d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
5 | f1oeq2 6607 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶)) | |
6 | 4, 5 | syl 17 | . 2 ⊢ (𝜑 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶)) |
7 | f1eq123d.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
8 | f1oeq3 6608 | . . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) | |
9 | 7, 8 | syl 17 | . 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
10 | 3, 6, 9 | 3bitrd 308 | 1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1542 –1-1-onto→wf1o 6338 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-un 3848 df-in 3850 df-ss 3860 df-sn 4517 df-pr 4519 df-op 4523 df-br 5031 df-opab 5093 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 |
This theorem is referenced by: f1oprswap 6661 f1oprg 6662 f1ossf1o 6900 cnfcom 9236 ackbij2lem2 9740 idffth 17308 ressffth 17313 symgval 18615 symg1bas 18637 symg2bas 18639 symgfixels 18680 symgfixelsi 18681 rhmf1o 19606 mat1f1o 21229 ushgredgedg 27171 ushgredgedgloop 27173 trlreslem 27641 wlknwwlksnbij 27826 wwlksnextbij 27840 clwlknf1oclwwlkn 28021 eupth0 28151 eupthp1 28153 foresf1o 30424 f1ocnt 30698 symgcom 30929 cycpmcl 30960 cycpmconjslem2 30999 nsgqusf1o 31173 dimkerim 31280 indf1ofs 31564 eulerpartgbij 31909 eulerpartlemn 31918 reprpmtf1o 32176 poimirlem16 35416 poimirlem17 35417 poimirlem19 35419 poimirlem20 35420 poimirlem28 35428 metakunt17 39732 wessf1ornlem 42260 disjf1o 42267 ssnnf1octb 42271 sge0fodjrnlem 43496 f1oresf1orab 44314 isomgr 44809 rnghmf1o 44995 |
Copyright terms: Public domain | W3C validator |