![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > spcv | GIF version |
Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.) |
Ref | Expression |
---|---|
spcv.1 | ⊢ 𝐴 ∈ V |
spcv.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcv | ⊢ (∀𝑥𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spcv.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | spcv.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | spcgv 2728 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓)) |
4 | 1, 3 | ax-mp 7 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1297 = wceq 1299 ∈ wcel 1448 Vcvv 2641 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 |
This theorem is referenced by: morex 2821 exmidexmid 4060 exmidsssn 4063 exmidel 4066 rext 4075 ontr2exmid 4378 regexmidlem1 4386 reg2exmid 4389 relop 4627 disjxp1 6063 rdgtfr 6201 ssfiexmid 6699 domfiexmid 6701 diffitest 6710 findcard 6711 fiintim 6746 fisseneq 6749 finomni 6924 exmidomni 6926 exmidlpo 6927 exmidunben 11731 bj-d0clsepcl 12708 bj-inf2vnlem1 12753 |
Copyright terms: Public domain | W3C validator |