![]() |
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 2920 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
3 | vtoclgaf.2 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
4 | 2, 3 | nfim 1900 | . . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
5 | eleq1 2822 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
6 | vtoclgaf.3 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
7 | 5, 6 | imbi12d 345 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
8 | vtoclgaf.4 | . . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑) | |
9 | 1, 4, 7, 8 | vtoclgf 3525 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓)) |
10 | 9 | pm2.43i 52 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 Ⅎwnf 1786 ∈ wcel 2107 Ⅎwnfc 2884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-v 3449 |
This theorem is referenced by: ssiun2s 5012 iunopeqop 5482 fvmptss 6964 fvmptf 6973 fmptco 7079 tfis 7795 inar1 10719 sumss 15617 fprodn0 15870 prmind2 16569 lss1d 20468 itg2splitlem 25136 dgrle 25627 cnlnadjlem5 31062 poimirlem25 36153 stoweidlem26 44357 |
Copyright terms: Public domain | W3C validator |