![]() |
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 2402 with a disjoint variable condition, which does not require ax-13 2375. See cbvexvw 2034 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2404 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 1855 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
3 | cbvalv1.nf2 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | nfn 1855 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
5 | cbvalv1.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 5 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
7 | 2, 4, 6 | cbvalv1 2342 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
8 | alnex 1778 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
9 | alnex 1778 | . . 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 1535 ∃wex 1776 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-11 2155 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1777 df-nf 1781 |
This theorem is referenced by: sb8ef 2356 exsb 2360 mof 2561 euf 2574 cbveuw 2604 eqvincf 3650 rexab2 3708 euabsn 4731 eluniab 4926 cbvopab1 5223 cbvopab1g 5224 cbvopab2 5225 cbvopab1s 5226 axrep1 5286 axrep2 5288 axrep4OLD 5292 opeliunxp 5756 dfdmf 5910 dfrnf 5964 elrnmpt1 5974 cbvoprab1 7520 cbvoprab2 7521 opabex3d 7989 opabex3rd 7990 opabex3 7991 zfcndrep 10652 fsum2dlem 15803 fprod2dlem 16013 2ndresdju 32666 bnj1146 34784 bnj607 34909 bnj1228 35004 fineqvrep 35088 poimirlem26 37633 sbcexf 38102 elunif 44954 stoweidlem46 46002 opeliun2xp 48178 |
Copyright terms: Public domain | W3C validator |