Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralrnmptw | Structured version Visualization version GIF version |
Description: A restricted quantifier over an image set. Version of ralrnmpt 6862 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by Gino Giotto, 26-Jan-2024.) |
Ref | Expression |
---|---|
ralrnmptw.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
ralrnmptw.2 | ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralrnmptw | ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrnmptw.1 | . . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | 1 | fnmpt 6488 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) |
3 | dfsbcq 3774 | . . . . 5 ⊢ (𝑤 = (𝐹‘𝑧) → ([𝑤 / 𝑦]𝜓 ↔ [(𝐹‘𝑧) / 𝑦]𝜓)) | |
4 | 3 | ralrn 6854 | . . . 4 ⊢ (𝐹 Fn 𝐴 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓)) |
5 | 2, 4 | syl 17 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓)) |
6 | nfsbc1v 3792 | . . . 4 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜓 | |
7 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑤𝜓 | |
8 | sbceq2a 3784 | . . . 4 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑦]𝜓 ↔ 𝜓)) | |
9 | 6, 7, 8 | cbvralw 3441 | . . 3 ⊢ (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑦 ∈ ran 𝐹𝜓) |
10 | nfmpt1 5164 | . . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | |
11 | 1, 10 | nfcxfr 2975 | . . . . . 6 ⊢ Ⅎ𝑥𝐹 |
12 | nfcv 2977 | . . . . . 6 ⊢ Ⅎ𝑥𝑧 | |
13 | 11, 12 | nffv 6680 | . . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝑧) |
14 | nfv 1915 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
15 | 13, 14 | nfsbcw 3794 | . . . 4 ⊢ Ⅎ𝑥[(𝐹‘𝑧) / 𝑦]𝜓 |
16 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑧[(𝐹‘𝑥) / 𝑦]𝜓 | |
17 | fveq2 6670 | . . . . 5 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) | |
18 | 17 | sbceq1d 3777 | . . . 4 ⊢ (𝑧 = 𝑥 → ([(𝐹‘𝑧) / 𝑦]𝜓 ↔ [(𝐹‘𝑥) / 𝑦]𝜓)) |
19 | 15, 16, 18 | cbvralw 3441 | . . 3 ⊢ (∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓) |
20 | 5, 9, 19 | 3bitr3g 315 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓)) |
21 | 1 | fvmpt2 6779 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐹‘𝑥) = 𝐵) |
22 | 21 | sbceq1d 3777 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ [𝐵 / 𝑦]𝜓)) |
23 | ralrnmptw.2 | . . . . . . 7 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | |
24 | 23 | sbcieg 3810 | . . . . . 6 ⊢ (𝐵 ∈ 𝑉 → ([𝐵 / 𝑦]𝜓 ↔ 𝜒)) |
25 | 24 | adantl 484 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([𝐵 / 𝑦]𝜓 ↔ 𝜒)) |
26 | 22, 25 | bitrd 281 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒)) |
27 | 26 | ralimiaa 3159 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒)) |
28 | ralbi 3167 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒) → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | |
29 | 27, 28 | syl 17 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
30 | 20, 29 | bitrd 281 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ∀wral 3138 [wsbc 3772 ↦ cmpt 5146 ran crn 5556 Fn wfn 6350 ‘cfv 6355 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-iota 6314 df-fun 6357 df-fn 6358 df-fv 6363 |
This theorem is referenced by: rexrnmptw 6861 ac6num 9901 gsumwspan 18011 dfod2 18691 ordtbaslem 21796 ordtrest2lem 21811 cncmp 22000 comppfsc 22140 ptpjopn 22220 ordthmeolem 22409 tsmsfbas 22736 tsmsf1o 22753 prdsxmetlem 22978 prdsbl 23101 metdsf 23456 metdsge 23457 minveclem1 24027 minveclem3b 24031 minveclem6 24037 mbflimsup 24267 xrlimcnp 25546 minvecolem1 28651 minvecolem5 28658 minvecolem6 28659 ordtrest2NEWlem 31165 cvmsss2 32521 fin2so 34894 prdsbnd 35086 rrnequiv 35128 ralrnmpt3 41551 |
Copyright terms: Public domain | W3C validator |