![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvexv1 | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2406 with a disjoint variable condition, which does not require ax-13 2379. See cbvexvw 2044 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2408 for another variant. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 31-May-2019.) |
Ref | Expression |
---|---|
cbvalv1.nf1 | ⊢ Ⅎ𝑦𝜑 |
cbvalv1.nf2 | ⊢ Ⅎ𝑥𝜓 |
cbvalv1.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvexv1 | ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvalv1.nf1 | . . . . 5 ⊢ Ⅎ𝑦𝜑 | |
2 | 1 | nfn 1858 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
3 | cbvalv1.nf2 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | nfn 1858 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
5 | cbvalv1.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 5 | notbid 321 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
7 | 2, 4, 6 | cbvalv1 2350 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
8 | 7 | notbii 323 | . 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓) |
9 | df-ex 1782 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
10 | df-ex 1782 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
11 | 8, 9, 10 | 3bitr4i 306 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∀wal 1536 ∃wex 1781 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-11 2158 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 |
This theorem is referenced by: sb8ev 2363 exsb 2367 mof 2622 euf 2636 cbveuw 2666 clelab 2933 issetf 3454 eqvincf 3591 rexab2 3639 rexab2OLD 3640 euabsn 4622 eluniab 4815 cbvopab1 5103 cbvopab1g 5104 cbvopab2 5105 cbvopab1s 5106 axrep1 5155 axrep2 5157 axrep4 5159 opeliunxp 5583 dfdmf 5729 dfrnf 5784 elrnmpt1 5794 cbvoprab1 7220 cbvoprab2 7221 opabex3d 7648 opabex3rd 7649 opabex3 7650 zfcndrep 10025 fsum2dlem 15117 fprod2dlem 15326 2ndresdju 30411 bnj1146 32173 bnj607 32298 bnj1228 32393 poimirlem26 35083 sbcexf 35553 elunif 41645 stoweidlem46 42688 opeliun2xp 44734 |
Copyright terms: Public domain | W3C validator |