![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > spcgv | Structured version Visualization version GIF version |
Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2137, ax-11 2154. (Revised by Wolf Lammen, 25-Aug-2023.) |
Ref | Expression |
---|---|
spcgv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcgv | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3492 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | id 22 | . . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V) | |
3 | spcgv.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | adantl 482 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓)) |
5 | 2, 4 | spcdv 3584 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓)) |
6 | 1, 5 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1539 = wceq 1541 ∈ wcel 2106 Vcvv 3474 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 |
This theorem is referenced by: spcv 3595 mob2 3711 sbceqal 3843 intss1 4967 dfiin2g 5035 alxfr 5405 friOLD 5637 funmo 6563 isofrlem 7336 tfisi 7847 limomss 7859 nnlim 7868 f1oweALT 7958 pssnn 9167 pssnnOLD 9264 findcard3 9284 findcard3OLD 9285 frmin 9743 ttukeylem1 10503 rami 16947 ramcl 16961 islbs3 20767 mplsubglem 21557 mpllsslem 21558 uniopn 22398 chlimi 30482 iinabrex 31795 dfon2lem3 34752 dfon2lem8 34757 neificl 36616 ismrcd1 41426 mnuop23d 43015 |
Copyright terms: Public domain | W3C validator |