![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralrnmpt | Structured version Visualization version GIF version |
Description: A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Ref | Expression |
---|---|
ralrnmpt.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
ralrnmpt.2 | ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralrnmpt | ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrnmpt.1 | . . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | 1 | fnmpt 6348 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) |
3 | dfsbcq 3703 | . . . . 5 ⊢ (𝑤 = (𝐹‘𝑧) → ([𝑤 / 𝑦]𝜓 ↔ [(𝐹‘𝑧) / 𝑦]𝜓)) | |
4 | 3 | ralrn 6710 | . . . 4 ⊢ (𝐹 Fn 𝐴 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓)) |
5 | 2, 4 | syl 17 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓)) |
6 | nfv 1890 | . . . . 5 ⊢ Ⅎ𝑤𝜓 | |
7 | nfsbc1v 3721 | . . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜓 | |
8 | sbceq1a 3712 | . . . . 5 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑦]𝜓)) | |
9 | 6, 7, 8 | cbvral 3396 | . . . 4 ⊢ (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓) |
10 | 9 | bicomi 225 | . . 3 ⊢ (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑦 ∈ ran 𝐹𝜓) |
11 | nfmpt1 5052 | . . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | |
12 | 1, 11 | nfcxfr 2945 | . . . . . 6 ⊢ Ⅎ𝑥𝐹 |
13 | nfcv 2947 | . . . . . 6 ⊢ Ⅎ𝑥𝑧 | |
14 | 12, 13 | nffv 6540 | . . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝑧) |
15 | nfv 1890 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
16 | 14, 15 | nfsbc 3723 | . . . 4 ⊢ Ⅎ𝑥[(𝐹‘𝑧) / 𝑦]𝜓 |
17 | nfv 1890 | . . . 4 ⊢ Ⅎ𝑧[(𝐹‘𝑥) / 𝑦]𝜓 | |
18 | fveq2 6530 | . . . . 5 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) | |
19 | 18 | sbceq1d 3706 | . . . 4 ⊢ (𝑧 = 𝑥 → ([(𝐹‘𝑧) / 𝑦]𝜓 ↔ [(𝐹‘𝑥) / 𝑦]𝜓)) |
20 | 16, 17, 19 | cbvral 3396 | . . 3 ⊢ (∀𝑧 ∈ 𝐴 [(𝐹‘𝑧) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓) |
21 | 5, 10, 20 | 3bitr3g 314 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓)) |
22 | 1 | fvmpt2 6636 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐹‘𝑥) = 𝐵) |
23 | 22 | sbceq1d 3706 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ [𝐵 / 𝑦]𝜓)) |
24 | ralrnmpt.2 | . . . . . . 7 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | |
25 | 24 | sbcieg 3734 | . . . . . 6 ⊢ (𝐵 ∈ 𝑉 → ([𝐵 / 𝑦]𝜓 ↔ 𝜒)) |
26 | 25 | adantl 482 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([𝐵 / 𝑦]𝜓 ↔ 𝜒)) |
27 | 23, 26 | bitrd 280 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒)) |
28 | 27 | ralimiaa 3124 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒)) |
29 | ralbi 3132 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ([(𝐹‘𝑥) / 𝑦]𝜓 ↔ 𝜒) → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | |
30 | 28, 29 | syl 17 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 [(𝐹‘𝑥) / 𝑦]𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
31 | 21, 30 | bitrd 280 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1520 ∈ wcel 2079 ∀wral 3103 [wsbc 3701 ↦ cmpt 5035 ran crn 5436 Fn wfn 6212 ‘cfv 6217 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ral 3108 df-rex 3109 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-br 4957 df-opab 5019 df-mpt 5036 df-id 5340 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-iota 6181 df-fun 6219 df-fn 6220 df-fv 6225 |
This theorem is referenced by: rexrnmpt 6717 ac6num 9736 gsumwspan 17810 dfod2 18409 ordtbaslem 21468 ordtrest2lem 21483 cncmp 21672 comppfsc 21812 ptpjopn 21892 ordthmeolem 22081 tsmsfbas 22407 tsmsf1o 22424 prdsxmetlem 22649 prdsbl 22772 metdsf 23127 metdsge 23128 minveclem1 23698 minveclem3b 23702 minveclem6 23708 mbflimsup 23938 xrlimcnp 25216 minvecolem1 28330 minvecolem5 28337 minvecolem6 28338 ordtrest2NEWlem 30738 cvmsss2 32085 fin2so 34356 prdsbnd 34549 rrnequiv 34591 ralrnmpt3 41025 |
Copyright terms: Public domain | W3C validator |