| 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 2141, ax-11 2157. (Revised by Wolf Lammen, 25-Aug-2023.) |
| Ref | Expression |
|---|---|
| spcgv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| spcgv | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elex 3501 | . 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 1538 = wceq 1540 ∈ wcel 2108 Vcvv 3480 |
| 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 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 |
| This theorem is referenced by: spcv 3605 mob2 3721 sbceqal 3851 intss1 4963 dfiin2g 5032 alxfr 5407 friOLD 5643 funmo 6581 isofrlem 7360 tfisi 7880 limomss 7892 nnlim 7901 f1oweALT 7997 pssnn 9208 findcard3 9318 findcard3OLD 9319 frmin 9789 ttukeylem1 10549 rami 17053 ramcl 17067 islbs3 21157 mplsubglem 22019 mpllsslem 22020 uniopn 22903 chlimi 31253 iinabrex 32582 dfon2lem3 35786 dfon2lem8 35791 neificl 37760 hashnexinj 42129 ismrcd1 42709 mnuop23d 44285 relpfrlem 44974 modelaxreplem2 44996 |
| Copyright terms: Public domain | W3C validator |