Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rspc | 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 2440 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
2 | nfcv 2299 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfv 1508 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
4 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1552 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
6 | eleq1 2220 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
7 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
8 | 6, 7 | imbi12d 233 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
9 | 2, 5, 8 | spcgf 2794 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓))) |
10 | 9 | pm2.43a 51 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓)) |
11 | 1, 10 | syl5bi 151 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1333 = wceq 1335 Ⅎwnf 1440 ∈ wcel 2128 ∀wral 2435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ral 2440 df-v 2714 |
This theorem is referenced by: rspcv 2812 rspc2 2827 pofun 4272 omsinds 4581 fmptcof 5634 fliftfuns 5748 qliftfuns 6564 xpf1o 6789 finexdc 6847 ssfirab 6878 iunfidisj 6890 dcfi 6925 cc3 7188 lble 8818 exfzdc 10139 uzsinds 10341 sumeq2 11256 sumfct 11271 sumrbdclem 11274 summodclem3 11277 summodclem2a 11278 zsumdc 11281 fsumgcl 11283 fsum3 11284 fsumf1o 11287 isumss 11288 isumss2 11290 fsum3cvg2 11291 fsumadd 11303 isummulc2 11323 fsum2dlemstep 11331 fisumcom2 11335 fsumshftm 11342 fisum0diag2 11344 fsummulc2 11345 fsum00 11359 fsumabs 11362 fsumrelem 11368 fsumiun 11374 isumshft 11387 mertenslem2 11433 prodeq2 11454 prodrbdclem 11468 prodmodclem3 11472 prodmodclem2a 11473 zproddc 11476 fprodseq 11480 prodfct 11484 fprodf1o 11485 prodssdc 11486 fprodmul 11488 fprodm1s 11498 fprodp1s 11499 fprodabs 11513 fprodap0 11518 fprod2dlemstep 11519 fprodcom2fi 11523 fprodrec 11526 fprodap0f 11533 fprodle 11537 zsupcllemstep 11831 infssuzex 11835 bezoutlemmain 11881 ctiunctlemudc 12166 iuncld 12515 txcnp 12671 fsumcncntop 12956 bj-nntrans 13526 |
Copyright terms: Public domain | W3C validator |