![]() |
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 2139, ax-11 2155. (Revised by Wolf Lammen, 25-Aug-2023.) |
Ref | Expression |
---|---|
spcgv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcgv | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3499 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | id 22 | . . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V) | |
3 | spcgv.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | adantl 481 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓)) |
5 | 2, 4 | spcdv 3594 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓)) |
6 | 1, 5 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 = wceq 1537 ∈ wcel 2106 Vcvv 3478 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 |
This theorem is referenced by: spcv 3605 mob2 3724 sbceqal 3857 intss1 4968 dfiin2g 5037 alxfr 5413 friOLD 5647 funmo 6583 isofrlem 7360 tfisi 7880 limomss 7892 nnlim 7901 f1oweALT 7996 pssnn 9207 findcard3 9316 findcard3OLD 9317 frmin 9787 ttukeylem1 10547 rami 17049 ramcl 17063 islbs3 21175 mplsubglem 22037 mpllsslem 22038 uniopn 22919 chlimi 31263 iinabrex 32589 dfon2lem3 35767 dfon2lem8 35772 neificl 37740 hashnexinj 42110 ismrcd1 42686 mnuop23d 44262 modelaxreplem2 44944 |
Copyright terms: Public domain | W3C validator |