![]() |
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 7097 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 20-Aug-2015.) Avoid ax-13 2371. (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 6690 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) |
3 | dfsbcq 3779 | . . . . 5 ⊢ (𝑤 = (𝐹‘𝑧) → ([𝑤 / 𝑦]𝜓 ↔ [(𝐹‘𝑧) / 𝑦]𝜓)) | |
4 | 3 | ralrn 7089 | . . . 4 ⊢ (𝐹 Fn 𝐴 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓)) |
5 | 2, 4 | syl 17 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓)) |
6 | nfsbc1v 3797 | . . . 4 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜓 | |
7 | nfv 1917 | . . . 4 ⊢ Ⅎ𝑤𝜓 | |
8 | sbceq2a 3789 | . . . 4 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑦]𝜓 ↔ 𝜓)) | |
9 | 6, 7, 8 | cbvralw 3303 | . . 3 ⊢ (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑦 ∈ ran 𝐹𝜓) |
10 | nfmpt1 5256 | . . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | |
11 | 1, 10 | nfcxfr 2901 | . . . . . 6 ⊢ Ⅎ𝑥𝐹 |
12 | nfcv 2903 | . . . . . 6 ⊢ Ⅎ𝑥𝑧 | |
13 | 11, 12 | nffv 6901 | . . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝑧) |
14 | nfv 1917 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
15 | 13, 14 | nfsbcw 3799 | . . . 4 ⊢ Ⅎ𝑥[(𝐹‘𝑧) / 𝑦]𝜓 |
16 | nfv 1917 | . . . 4 ⊢ Ⅎ𝑧[(𝐹‘𝑥) / 𝑦]𝜓 | |
17 | fveq2 6891 | . . . . 5 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) | |
18 | 17 | sbceq1d 3782 | . . . 4 ⊢ (𝑧 = 𝑥 → ([(𝐹‘𝑧) / 𝑦]𝜓 ↔ [(𝐹‘𝑥) / 𝑦]𝜓)) |
19 | 15, 16, 18 | cbvralw 3303 | . . 3 ⊢ (∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓) |
20 | 5, 9, 19 | 3bitr3g 312 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓)) |
21 | 1 | fvmpt2 7009 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐹‘𝑥) = 𝐵) |
22 | 21 | sbceq1d 3782 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ [𝐵 / 𝑦]𝜓)) |
23 | ralrnmptw.2 | . . . . . . 7 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | |
24 | 23 | sbcieg 3817 | . . . . . 6 ⊢ (𝐵 ∈ 𝑉 → ([𝐵 / 𝑦]𝜓 ↔ 𝜒)) |
25 | 24 | adantl 482 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([𝐵 / 𝑦]𝜓 ↔ 𝜒)) |
26 | 22, 25 | bitrd 278 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒)) |
27 | 26 | ralimiaa 3082 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒)) |
28 | ralbi 3103 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒) → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | |
29 | 27, 28 | syl 17 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
30 | 20, 29 | bitrd 278 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 [wsbc 3777 ↦ cmpt 5231 ran crn 5677 Fn wfn 6538 ‘cfv 6543 |
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 5299 ax-nul 5306 ax-pr 5427 |
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-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-fv 6551 |
This theorem is referenced by: rexrnmptw 7096 ac6num 10476 gsumwspan 18729 dfod2 19434 ordtbaslem 22699 ordtrest2lem 22714 cncmp 22903 comppfsc 23043 ptpjopn 23123 ordthmeolem 23312 tsmsfbas 23639 tsmsf1o 23656 prdsxmetlem 23881 prdsbl 24007 metdsf 24371 metdsge 24372 minveclem1 24948 minveclem3b 24952 minveclem6 24958 mbflimsup 25190 xrlimcnp 26480 minvecolem1 30165 minvecolem5 30172 minvecolem6 30173 ordtrest2NEWlem 32971 cvmsss2 34334 fin2so 36561 prdsbnd 36747 rrnequiv 36789 ralrnmpt3 44042 |
Copyright terms: Public domain | W3C validator |