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 2401 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 321 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
3 | 2 | cbvalvw 2048 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
4 | 3 | notbii 323 | . 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓) |
5 | df-ex 1787 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
6 | df-ex 1787 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
7 | 4, 5, 6 | 3bitr4i 306 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∀wal 1540 ∃wex 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 |
This theorem is referenced by: cbvex2vw 2053 mojust 2539 mo4 2566 eujust 2572 cbveuvw 2607 clelab 2875 cbvrexvw 3350 cbvrexdva2 3359 euind 3623 reuind 3652 cbvopab2v 5108 bm1.3ii 5170 reusv2lem2 5266 relop 5693 dmcoss 5814 fv3 6694 exfo 6883 zfun 7482 suppimacnv 7871 wfrlem1 7985 ac6sfi 8838 brwdom2 9112 aceq1 9619 aceq0 9620 aceq3lem 9622 dfac4 9624 kmlem2 9653 kmlem13 9664 axdc4lem 9957 zfac 9962 zfcndun 10117 zfcndac 10121 sup2 11676 supmul 11692 climmo 15006 summo 15169 prodmo 15384 gsumval3eu 19145 elpt 22325 bnj1185 32346 fineqvac 32639 satf0op 32912 sat1el2xp 32914 frrlem1 33445 bj-bm1.3ii 34880 fdc 35548 sn-sup2 40038 cpcoll2d 41441 axc11next 41584 fnchoice 42132 ichexmpl1 44484 |
Copyright terms: Public domain | W3C validator |