| 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 2404 with a disjoint variable condition, which does not require ax-13 2377. See cbvexvw 2036 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2406 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 1857 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
| 3 | cbvalv1.nf2 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
| 4 | 3 | nfn 1857 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
| 5 | cbvalv1.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 6 | 5 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
| 7 | 2, 4, 6 | cbvalv1 2343 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
| 8 | alnex 1781 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
| 9 | alnex 1781 | . . 3 ⊢ (∀𝑦 ¬ 𝜓 ↔ ¬ ∃𝑦𝜓) | |
| 10 | 7, 8, 9 | 3bitr3i 301 | . 2 ⊢ (¬ ∃𝑥𝜑 ↔ ¬ ∃𝑦𝜓) |
| 11 | 10 | con4bii 321 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1538 ∃wex 1779 Ⅎwnf 1783 |
| 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-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: sb8ef 2358 exsb 2362 mof 2563 euf 2576 cbveuw 2606 eqvincf 3650 rexab2 3705 euabsn 4726 eluniab 4921 cbvopab1 5217 cbvopab1g 5218 cbvopab2 5219 cbvopab1s 5220 axrep1 5280 axrep2 5282 axrep4OLD 5286 opeliunxp 5752 opeliun2xp 5753 dfdmf 5907 dfrnf 5961 elrnmpt1 5971 cbvoprab1 7520 cbvoprab2 7521 opabex3d 7990 opabex3rd 7991 opabex3 7992 zfcndrep 10654 fsum2dlem 15806 fprod2dlem 16016 2ndresdju 32659 bnj1146 34805 bnj607 34930 bnj1228 35025 fineqvrep 35109 poimirlem26 37653 sbcexf 38122 elunif 45021 stoweidlem46 46061 |
| Copyright terms: Public domain | W3C validator |