![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclgf | Structured version Visualization version GIF version |
Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.) |
Ref | Expression |
---|---|
vtoclgf.1 | ⊢ Ⅎ𝑥𝐴 |
vtoclgf.2 | ⊢ Ⅎ𝑥𝜓 |
vtoclgf.3 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclgf.4 | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtoclgf | ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3340 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | vtoclgf.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | issetf 3336 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
4 | vtoclgf.2 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
5 | vtoclgf.4 | . . . . 5 ⊢ 𝜑 | |
6 | vtoclgf.3 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
7 | 5, 6 | mpbii 223 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝜓) |
8 | 4, 7 | exlimi 2221 | . . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓) |
9 | 3, 8 | sylbi 207 | . 2 ⊢ (𝐴 ∈ V → 𝜓) |
10 | 1, 9 | syl 17 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1620 ∃wex 1841 Ⅎwnf 1845 ∈ wcel 2127 Ⅎwnfc 2877 Vcvv 3328 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-v 3330 |
This theorem is referenced by: vtocl2gf 3396 vtocl3gf 3397 vtoclgaf 3399 elabgf 3476 fprodsplit1f 14891 ssiun2sf 29656 subtr 32585 subtr2 32586 supxrgere 40016 supxrgelem 40020 supxrge 40021 fsumsplit1 40276 fmuldfeqlem1 40286 fprodcnlem 40303 climsuse 40312 dvnmptdivc 40625 dvmptfprodlem 40631 stoweidlem59 40748 fourierdlem31 40827 sge0f1o 41071 sge0fodjrnlem 41105 salpreimagelt 41393 salpreimalegt 41395 |
Copyright terms: Public domain | W3C validator |