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 2145, ax-11 2161. (Revised by Wolf Lammen, 25-Aug-2023.) |
Ref | Expression |
---|---|
spcgv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcgv | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3512 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | id 22 | . . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V) | |
3 | spcgv.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | adantl 484 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓)) |
5 | 2, 4 | spcdv 3593 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓)) |
6 | 1, 5 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wal 1535 = wceq 1537 ∈ wcel 2114 Vcvv 3494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-v 3496 |
This theorem is referenced by: spcv 3606 mob2 3706 intss1 4891 dfiin2g 4957 alxfr 5308 fri 5517 isofrlem 7093 tfisi 7573 limomss 7585 nnlim 7593 f1oweALT 7673 pssnn 8736 findcard3 8761 ttukeylem1 9931 rami 16351 ramcl 16365 islbs3 19927 mplsubglem 20214 mpllsslem 20215 uniopn 21505 chlimi 29011 dfon2lem3 33030 dfon2lem8 33035 neificl 35043 ismrcd1 39315 mnuop23d 40622 |
Copyright terms: Public domain | W3C validator |