| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > vtoclgaf | Structured version Visualization version GIF version | ||
| Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.) |
| Ref | Expression |
|---|---|
| vtoclgaf.1 | ⊢ Ⅎ𝑥𝐴 |
| vtoclgaf.2 | ⊢ Ⅎ𝑥𝜓 |
| vtoclgaf.3 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| vtoclgaf.4 | ⊢ (𝑥 ∈ 𝐵 → 𝜑) |
| Ref | Expression |
|---|---|
| vtoclgaf | ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtoclgaf.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
| 2 | 1 | nfel1 2922 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
| 3 | vtoclgaf.2 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
| 4 | 2, 3 | nfim 1896 | . . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
| 5 | eleq1 2829 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
| 6 | vtoclgaf.3 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 7 | 5, 6 | imbi12d 344 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
| 8 | vtoclgaf.4 | . . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑) | |
| 9 | 1, 4, 7, 8 | vtoclgf 3569 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓)) |
| 10 | 9 | pm2.43i 52 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 Ⅎwnf 1783 ∈ wcel 2108 Ⅎwnfc 2890 |
| 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-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-v 3482 |
| This theorem is referenced by: vtocl2gaf 3579 vtocl3gaf 3581 ssiun2s 5048 iunopeqop 5526 fvmptss 7028 fvmptf 7037 fmptco 7149 tfis 7876 inar1 10815 sumss 15760 fprodn0 16015 prmind2 16722 lss1d 20961 itg2splitlem 25783 dgrle 26282 cnlnadjlem5 32090 poimirlem25 37652 stoweidlem26 46041 |
| Copyright terms: Public domain | W3C validator |