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 6040 | . . 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 6041 | . . 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 6042 | . . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) | |
9 | 7, 8 | syl 17 | . 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
10 | 3, 6, 9 | 3bitrd 293 | 1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 –1-1-onto→wf1o 5803 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 |
This theorem is referenced by: f1oprswap 6092 f1oprg 6093 cnfcom 8480 ackbij2lem2 8945 s2f1o 13511 s4f1o 13513 idffth 16416 ressffth 16421 symg1bas 17639 symg2bas 17641 symgfixels 17677 symgfixelsi 17678 rhmf1o 18555 mat1f1o 20103 isismt 25229 wwlkextbij 26261 foresf1o 28727 f1ocnt 28946 indf1ofs 29415 eulerpartgbij 29761 eulerpartlemn 29770 poimirlem16 32595 poimirlem17 32596 poimirlem19 32598 poimirlem20 32599 poimirlem28 32607 wessf1ornlem 38366 disjf1o 38373 ssnnf1octb 38377 sge0fodjrnlem 39309 ushgredgedga 40456 ushgredgedgaloop 40458 trlreslem 40907 wwlksnextbij 41108 eupth0 41382 eupthp1 41384 rnghmf1o 41693 |
Copyright terms: Public domain | W3C validator |