![]() |
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 2460 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
2 | nfcv 2319 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfv 1528 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
4 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1572 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
6 | eleq1 2240 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
7 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
8 | 6, 7 | imbi12d 234 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
9 | 2, 5, 8 | spcgf 2821 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓))) |
10 | 9 | pm2.43a 51 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓)) |
11 | 1, 10 | biimtrid 152 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∀wal 1351 = wceq 1353 Ⅎwnf 1460 ∈ wcel 2148 ∀wral 2455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-v 2741 |
This theorem is referenced by: rspcv 2839 rspc2 2854 rspc2vd 3127 pofun 4314 omsinds 4623 fmptcof 5686 fliftfuns 5802 qliftfuns 6622 xpf1o 6847 finexdc 6905 ssfirab 6936 iunfidisj 6948 dcfi 6983 cc3 7270 lble 8907 exfzdc 10243 uzsinds 10445 sumeq2 11370 sumfct 11385 sumrbdclem 11388 summodclem3 11391 summodclem2a 11392 zsumdc 11395 fsumgcl 11397 fsum3 11398 fsumf1o 11401 isumss 11402 isumss2 11404 fsum3cvg2 11405 fsumadd 11417 isummulc2 11437 fsum2dlemstep 11445 fisumcom2 11449 fsumshftm 11456 fisum0diag2 11458 fsummulc2 11459 fsum00 11473 fsumabs 11476 fsumrelem 11482 fsumiun 11488 isumshft 11501 mertenslem2 11547 prodeq2 11568 prodrbdclem 11582 prodmodclem3 11586 prodmodclem2a 11587 zproddc 11590 fprodseq 11594 prodfct 11598 fprodf1o 11599 prodssdc 11600 fprodmul 11602 fprodm1s 11612 fprodp1s 11613 fprodabs 11627 fprodap0 11632 fprod2dlemstep 11633 fprodcom2fi 11637 fprodrec 11640 fprodap0f 11647 fprodle 11651 zsupcllemstep 11949 infssuzex 11953 bezoutlemmain 12002 nnwosdc 12043 pcmpt 12344 ctiunctlemudc 12441 iuncld 13755 txcnp 13911 fsumcncntop 14196 bj-nntrans 14843 |
Copyright terms: Public domain | W3C validator |