![]() |
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 1824 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
3 | cbval.2 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | nfn 1824 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
5 | cbval.3 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 5 | notbid 307 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
7 | 2, 4, 6 | cbval 2307 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
8 | 7 | notbii 309 | . 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓) |
9 | df-ex 1745 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
10 | df-ex 1745 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
11 | 8, 9, 10 | 3bitr4i 292 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∀wal 1521 ∃wex 1744 Ⅎwnf 1748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ex 1745 df-nf 1750 |
This theorem is referenced by: cbvexvOLD 2312 sb8e 2453 exsb 2496 euf 2506 mo2 2507 cbvmo 2535 clelab 2777 issetf 3239 eqvincf 3362 rexab2 3406 euabsn 4293 eluniab 4479 cbvopab1 4756 cbvopab2 4757 cbvopab1s 4758 axrep1 4805 axrep2 4806 axrep4 4808 opeliunxp 5204 dfdmf 5349 dfrnf 5396 elrnmpt1 5406 cbvoprab1 6769 cbvoprab2 6770 opabex3d 7187 opabex3 7188 zfcndrep 9474 fsum2dlem 14545 fprod2dlem 14754 bnj1146 30988 bnj607 31112 bnj1228 31205 poimirlem26 33565 sbcexf 34048 elunif 39489 stoweidlem46 40581 opeliun2xp 42436 |
Copyright terms: Public domain | W3C validator |