| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rspc | Structured version Visualization version GIF version | ||
| Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) |
| Ref | Expression |
|---|---|
| rspc.1 | ⊢ Ⅎ𝑥𝜓 |
| rspc.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| rspc | ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
| 2 | nfcv 2905 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
| 3 | nfv 1914 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
| 4 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
| 5 | 3, 4 | nfim 1896 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
| 6 | eleq1 2829 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
| 7 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 8 | 6, 7 | imbi12d 344 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
| 9 | 2, 5, 8 | spcgf 3591 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓))) |
| 10 | 9 | pm2.43a 54 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓)) |
| 11 | 1, 10 | biimtrid 242 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 = wceq 1540 Ⅎwnf 1783 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 |
| This theorem is referenced by: rspc2 3631 rspc2vd 3947 disjxiun 5140 pofun 5610 fmptcof 7150 fliftfuns 7334 ofmpteq 7720 tfisg 7875 qliftfuns 8844 xpf1o 9179 iunfi 9383 iundom2g 10580 lble 12220 rlimcld2 15614 sumeq2ii 15729 summolem3 15750 zsum 15754 fsum 15756 fsumf1o 15759 sumss2 15762 fsumcvg2 15763 fsumadd 15776 isummulc2 15798 fsum2dlem 15806 fsumcom2 15810 fsumshftm 15817 fsum0diag2 15819 fsummulc2 15820 fsum00 15834 fsumabs 15837 fsumrelem 15843 fsumrlim 15847 fsumo1 15848 o1fsum 15849 fsumiun 15857 isumshft 15875 prodeq2ii 15947 prodmolem3 15969 zprod 15973 fprod 15977 fprodf1o 15982 prodss 15983 fprodser 15985 fprodmul 15996 fproddiv 15997 fprodm1s 16006 fprodp1s 16007 fprodabs 16010 fprod2dlem 16016 fprodcom2 16020 fprodefsum 16131 sumeven 16424 sumodd 16425 pcmpt 16930 invfuc 18022 dprd2d2 20064 txcnp 23628 ptcnplem 23629 prdsdsf 24377 prdsxmet 24379 fsumcn 24894 ovolfiniun 25536 ovoliunnul 25542 volfiniun 25582 iunmbl 25588 limciun 25929 dvfsumle 26060 dvfsumleOLD 26061 dvfsumabs 26063 dvfsumlem1 26066 dvfsumlem3 26069 dvfsumlem4 26070 dvfsumrlim 26072 dvfsumrlim2 26073 dvfsum2 26075 itgsubst 26090 fsumvma 27257 dchrisumlema 27532 dchrisumlem2 27534 dchrisumlem3 27535 nosupbnd1 27759 noinfbnd1 27774 chirred 32414 fsumiunle 32831 sigapildsyslem 34162 voliune 34230 volfiniune 34231 ptrest 37626 poimirlem25 37652 poimirlem26 37653 mzpsubst 42759 rabdiophlem2 42813 cvgcaule 45502 etransclem48 46297 sge0iunmpt 46433 2reu8i 47125 |
| Copyright terms: Public domain | W3C validator |