![]() |
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 2738 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵)) | |
2 | 1 | anbi2d 628 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))) |
3 | df-fo 6560 | . 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴)) | |
4 | df-fo 6560 | . 2 ⊢ (𝐹:𝐶–onto→𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 313 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 ran crn 5683 Fn wfn 6549 –onto→wfo 6552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-fo 6560 |
This theorem is referenced by: fimadmfo 6824 f1oeq3 6833 foeq123d 6836 resdif 6864 ncanth 7378 ffoss 7959 rneqdmfinf1o 9375 fidomdm 9376 fifo 9475 brwdom 9610 brwdom2 9616 canthwdom 9622 ixpiunwdom 9633 fin1a2lem7 10449 dmct 10567 znnen 16214 quslem 17558 znzrhfo 21545 rncmp 23391 connima 23420 conncn 23421 qtopcmplem 23702 qtoprest 23712 eupths 30133 pjhfo 31639 2ndresdjuf1o 32567 cycpmconjvlem 33019 algextdeglem8 33591 msrfo 35374 ivthALT 36047 bj-inftyexpitaufo 36909 poimirlem26 37347 poimirlem27 37348 opidon2OLD 37555 founiiun0 44797 focofob 46693 fundcmpsurinj 46981 fundcmpsurbijinj 46982 fullthinc 48367 |
Copyright terms: Public domain | W3C validator |