![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralrn | Structured version Visualization version GIF version |
Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.) |
Ref | Expression |
---|---|
rexrn.1 | ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ralrn | ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvexd 6907 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V) | |
2 | fvelrnb 6953 | . . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥)) | |
3 | eqcom 2740 | . . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦)) | |
4 | 3 | rexbii 3095 | . . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)) |
5 | 2, 4 | bitrdi 287 | . 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))) |
6 | rexrn.1 | . . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) | |
7 | 6 | adantl 483 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓)) |
8 | 1, 5, 7 | ralxfr2d 5409 | 1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ran crn 5678 Fn wfn 6539 ‘cfv 6544 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-iota 6496 df-fun 6546 df-fn 6547 df-fv 6552 |
This theorem is referenced by: ralrnmptw 7096 ralrnmpt 7098 cbvfo 7287 isoselem 7338 indexfi 9360 ordtypelem9 9521 ordtypelem10 9522 wemapwe 9692 numacn 10044 acndom 10046 rpnnen1lem3 12963 fsequb2 13941 limsuple 15422 limsupval2 15424 climsup 15616 ruclem11 16183 ruclem12 16184 prmreclem6 16854 imasaddfnlem 17474 imasvscafn 17483 cycsubgcl 19083 ghmrn 19105 ghmnsgima 19116 pgpssslw 19482 gexex 19721 dprdfcntz 19885 znf1o 21107 frlmlbs 21352 lindfrn 21376 ptcnplem 23125 kqt0lem 23240 isr0 23241 regr1lem2 23244 uzrest 23401 tmdgsum2 23600 imasf1oxmet 23881 imasf1omet 23882 bndth 24474 evth 24475 ovolficcss 24986 ovollb2lem 25005 ovolunlem1 25014 ovoliunlem1 25019 ovoliunlem2 25020 ovoliun2 25023 ovolscalem1 25030 ovolicc1 25033 voliunlem2 25068 voliunlem3 25069 ioombl1lem4 25078 uniioovol 25096 uniioombllem2 25100 uniioombllem3 25102 uniioombllem6 25105 volsup2 25122 vitalilem3 25127 mbfsup 25181 mbfinf 25182 mbflimsup 25183 itg1ge0 25203 itg1mulc 25222 itg1climres 25232 mbfi1fseqlem4 25236 itg2seq 25260 itg2monolem1 25268 itg2mono 25271 itg2i1fseq2 25274 itg2gt0 25278 itg2cnlem1 25279 itg2cn 25281 limciun 25411 plycpn 25802 hmopidmchi 31404 hmopidmpji 31405 rge0scvg 32929 mclsax 34560 mblfinlem2 36526 ismtyhmeolem 36672 nacsfix 41450 fnwe2lem2 41793 gneispace 42885 climinf 44322 liminfval2 44484 |
Copyright terms: Public domain | W3C validator |