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 2144, ax-11 2160. (Revised by Wolf Lammen, 25-Aug-2023.) |
Ref | Expression |
---|---|
spcgv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcgv | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3515 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | id 22 | . . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V) | |
3 | spcgv.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | adantl 484 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓)) |
5 | 2, 4 | spcdv 3596 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓)) |
6 | 1, 5 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wal 1534 = wceq 1536 ∈ wcel 2113 Vcvv 3497 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1780 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-v 3499 |
This theorem is referenced by: spcv 3609 mob2 3709 intss1 4894 dfiin2g 4960 alxfr 5311 fri 5520 isofrlem 7096 tfisi 7576 limomss 7588 nnlim 7596 f1oweALT 7676 pssnn 8739 findcard3 8764 ttukeylem1 9934 rami 16354 ramcl 16368 islbs3 19930 mplsubglem 20217 mpllsslem 20218 uniopn 21508 chlimi 29014 dfon2lem3 33034 dfon2lem8 33039 neificl 35032 ismrcd1 39301 mnuop23d 40608 |
Copyright terms: Public domain | W3C validator |