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 2410 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 319 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
3 | 2 | cbvalvw 2034 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
4 | 3 | notbii 321 | . 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓) |
5 | df-ex 1772 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
6 | df-ex 1772 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
7 | 4, 5, 6 | 3bitr4i 304 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∀wal 1526 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 |
This theorem is referenced by: cbvex2vw 2039 mojust 2614 mo4 2643 eujust 2649 cbvrexvw 3448 cbvrexdva2 3455 elisset 3503 euind 3712 reuind 3741 cbvopab2v 5135 bm1.3ii 5197 reusv2lem2 5290 relop 5714 dmcoss 5835 fv3 6681 exfo 6863 zfun 7451 suppimacnv 7830 wfrlem1 7943 ac6sfi 8750 brwdom2 9025 aceq1 9531 aceq0 9532 aceq3lem 9534 dfac4 9536 kmlem2 9565 kmlem13 9576 axdc4lem 9865 zfac 9870 zfcndun 10025 zfcndac 10029 sup2 11585 supmul 11601 climmo 14902 summo 15062 prodmo 15278 gsumval3eu 18953 elpt 22108 bnj1185 31964 satf0op 32521 sat1el2xp 32523 frrlem1 33020 bj-bm1.3ii 34251 fdc 34901 cpcoll2d 40472 axc11next 40615 fnchoice 41163 ichexmpl1 43508 |
Copyright terms: Public domain | W3C validator |