![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > foeq3 | Structured version Visualization version GIF version |
Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
foeq3 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2747 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵)) | |
2 | 1 | anbi2d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))) |
3 | df-fo 6569 | . 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴)) | |
4 | df-fo 6569 | . 2 ⊢ (𝐹:𝐶–onto→𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ran crn 5690 Fn wfn 6558 –onto→wfo 6561 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-fo 6569 |
This theorem is referenced by: fimadmfo 6830 f1oeq3 6839 foeq123d 6842 resdif 6870 ncanth 7386 ffoss 7969 rneqdmfinf1o 9371 fidomdm 9372 fifo 9470 brwdom 9605 brwdom2 9611 canthwdom 9617 ixpiunwdom 9628 fin1a2lem7 10444 dmct 10562 s7f1o 15002 znnen 16245 quslem 17590 znzrhfo 21584 rncmp 23420 connima 23449 conncn 23450 qtopcmplem 23731 qtoprest 23741 eupths 30229 pjhfo 31735 2ndresdjuf1o 32667 cycpmconjvlem 33144 algextdeglem8 33730 msrfo 35531 ivthALT 36318 bj-inftyexpitaufo 37185 poimirlem26 37633 poimirlem27 37634 opidon2OLD 37841 founiiun0 45133 focofob 47030 fundcmpsurinj 47334 fundcmpsurbijinj 47335 fullthinc 48846 |
Copyright terms: Public domain | W3C validator |