| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cbvexvw | Structured version Visualization version GIF version | ||
| Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2406 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.) |
| Ref | Expression |
|---|---|
| cbvalvw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| cbvexvw | ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvalvw.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 2 | 1 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
| 3 | 2 | cbvalvw 2035 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
| 4 | 3 | notbii 320 | . 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓) |
| 5 | df-ex 1780 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
| 6 | df-ex 1780 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
| 7 | 4, 5, 6 | 3bitr4i 303 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1538 ∃wex 1779 |
| 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: cbvex2vw 2040 mojust 2539 mo4 2566 eujust 2571 cbveuvw 2605 iseqsetvlem 2805 cbvrexvw 3238 cbvrexdva2OLD 3350 euind 3730 reuind 3759 cbvopab1v 5221 cbvopab2v 5223 bm1.3iiOLD 5302 reusv2lem2 5399 relop 5861 dmcoss 5985 fv3 6924 exfo 7125 cbvoprab3v 7525 zfun 7756 suppimacnv 8199 frrlem1 8311 wfrlem1OLD 8348 ac6sfi 9320 brwdom2 9613 ttrclss 9760 ttrclselem2 9766 aceq1 10157 aceq0 10158 aceq3lem 10160 dfac4 10162 kmlem2 10192 kmlem13 10203 axdc4lem 10495 zfac 10500 zfcndun 10655 zfcndac 10659 sup2 12224 supmul 12240 climmo 15593 summo 15753 prodmo 15972 gsumval3eu 19922 elpt 23580 gsumwrd2dccatlem 33069 1arithidomlem1 33563 1arithidom 33565 bnj1185 34807 fineqvac 35111 satf0op 35382 sat1el2xp 35384 cbvrexvw2 36228 cbvoprab1vw 36238 cbvoprab2vw 36239 cbvoprab13vw 36242 bj-bm1.3ii 37065 wl-ax12v2cl 37507 fdc 37752 sn-sup2 42501 cpcoll2d 44278 axc11next 44425 fnchoice 45034 ichexmpl1 47456 |
| Copyright terms: Public domain | W3C validator |