![]() |
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 6903 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V) | |
2 | fvelrnb 6949 | . . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥)) | |
3 | eqcom 2739 | . . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦)) | |
4 | 3 | rexbii 3094 | . . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)) |
5 | 2, 4 | bitrdi 286 | . 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))) |
6 | rexrn.1 | . . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) | |
7 | 6 | adantl 482 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓)) |
8 | 1, 5, 7 | ralxfr2d 5407 | 1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 ∃wrex 3070 Vcvv 3474 ran crn 5676 Fn wfn 6535 ‘cfv 6540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-iota 6492 df-fun 6542 df-fn 6543 df-fv 6548 |
This theorem is referenced by: ralrnmptw 7092 ralrnmpt 7094 cbvfo 7283 isoselem 7334 indexfi 9356 ordtypelem9 9517 ordtypelem10 9518 wemapwe 9688 numacn 10040 acndom 10042 rpnnen1lem3 12959 fsequb2 13937 limsuple 15418 limsupval2 15420 climsup 15612 ruclem11 16179 ruclem12 16180 prmreclem6 16850 imasaddfnlem 17470 imasvscafn 17479 cycsubgcl 19077 ghmrn 19099 ghmnsgima 19110 pgpssslw 19476 gexex 19715 dprdfcntz 19879 znf1o 21098 frlmlbs 21343 lindfrn 21367 ptcnplem 23116 kqt0lem 23231 isr0 23232 regr1lem2 23235 uzrest 23392 tmdgsum2 23591 imasf1oxmet 23872 imasf1omet 23873 bndth 24465 evth 24466 ovolficcss 24977 ovollb2lem 24996 ovolunlem1 25005 ovoliunlem1 25010 ovoliunlem2 25011 ovoliun2 25014 ovolscalem1 25021 ovolicc1 25024 voliunlem2 25059 voliunlem3 25060 ioombl1lem4 25069 uniioovol 25087 uniioombllem2 25091 uniioombllem3 25093 uniioombllem6 25096 volsup2 25113 vitalilem3 25118 mbfsup 25172 mbfinf 25173 mbflimsup 25174 itg1ge0 25194 itg1mulc 25213 itg1climres 25223 mbfi1fseqlem4 25227 itg2seq 25251 itg2monolem1 25259 itg2mono 25262 itg2i1fseq2 25265 itg2gt0 25269 itg2cnlem1 25270 itg2cn 25272 limciun 25402 plycpn 25793 hmopidmchi 31391 hmopidmpji 31392 rge0scvg 32917 mclsax 34548 mblfinlem2 36514 ismtyhmeolem 36660 nacsfix 41435 fnwe2lem2 41778 gneispace 42870 climinf 44308 liminfval2 44470 |
Copyright terms: Public domain | W3C validator |