Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbvex | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
cbval.1 | ⊢ Ⅎ𝑦𝜑 |
cbval.2 | ⊢ Ⅎ𝑥𝜓 |
cbval.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvex | ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbval.1 | . . . . 5 ⊢ Ⅎ𝑦𝜑 | |
2 | 1 | nfn 1768 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
3 | cbval.2 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | nfn 1768 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
5 | cbval.3 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 5 | notbid 307 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
7 | 2, 4, 6 | cbval 2259 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
8 | 7 | notbii 309 | . 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓) |
9 | df-ex 1696 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
10 | df-ex 1696 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
11 | 8, 9, 10 | 3bitr4i 291 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∀wal 1473 ∃wex 1695 Ⅎwnf 1699 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-ex 1696 df-nf 1701 |
This theorem is referenced by: cbvexvOLD 2264 sb8e 2413 exsb 2456 euf 2466 mo2 2467 cbvmo 2494 clelab 2735 issetf 3181 eqvincf 3301 rexab2 3340 euabsn 4205 eluniab 4383 cbvopab1 4655 cbvopab2 4656 cbvopab1s 4657 axrep1 4700 axrep2 4701 axrep4 4703 opeliunxp 5093 dfdmf 5239 dfrnf 5285 elrnmpt1 5295 cbvoprab1 6625 cbvoprab2 6626 opabex3d 7037 opabex3 7038 zfcndrep 9315 fsum2dlem 14343 fprod2dlem 14549 bnj1146 30116 bnj607 30240 bnj1228 30333 poimirlem26 32605 sbcexf 33088 elunif 38198 stoweidlem46 38939 opeliun2xp 41904 |
Copyright terms: Public domain | W3C validator |