![]() |
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 2400 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 2040 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
4 | 3 | notbii 320 | . 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓) |
5 | df-ex 1783 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
6 | df-ex 1783 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
7 | 4, 5, 6 | 3bitr4i 303 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∀wal 1540 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 |
This theorem is referenced by: cbvex2vw 2045 mojust 2538 mo4 2565 eujust 2570 cbveuvw 2605 clelab 2884 cbvrexvw 3229 cbvrexdva2OLD 3328 euind 3687 reuind 3716 cbvopab1v 5189 cbvopab2v 5191 bm1.3ii 5264 reusv2lem2 5359 relop 5811 dmcoss 5931 fv3 6865 exfo 7060 zfun 7678 suppimacnv 8110 frrlem1 8222 wfrlem1OLD 8259 ac6sfi 9238 brwdom2 9516 ttrclss 9663 ttrclselem2 9669 aceq1 10060 aceq0 10061 aceq3lem 10063 dfac4 10065 kmlem2 10094 kmlem13 10105 axdc4lem 10398 zfac 10403 zfcndun 10558 zfcndac 10562 sup2 12118 supmul 12134 climmo 15446 summo 15609 prodmo 15826 gsumval3eu 19688 elpt 22939 bnj1185 33445 fineqvac 33738 satf0op 34011 sat1el2xp 34013 bj-bm1.3ii 35564 fdc 36233 sn-sup2 40967 cpcoll2d 42613 axc11next 42760 fnchoice 43308 ichexmpl1 45735 |
Copyright terms: Public domain | W3C validator |