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 2402 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 1537 ∃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 397 df-ex 1783 |
This theorem is referenced by: cbvex2vw 2045 mojust 2540 mo4 2567 eujust 2572 cbveuvw 2607 clelab 2884 cbvrexvw 3385 cbvrexdva2 3394 euind 3660 reuind 3689 cbvopab1v 5154 cbvopab2v 5156 bm1.3ii 5227 reusv2lem2 5323 relop 5762 dmcoss 5883 fv3 6801 exfo 6990 zfun 7598 suppimacnv 7999 frrlem1 8111 wfrlem1OLD 8148 ac6sfi 9067 brwdom2 9341 ttrclss 9487 ttrclselem2 9493 aceq1 9882 aceq0 9883 aceq3lem 9885 dfac4 9887 kmlem2 9916 kmlem13 9927 axdc4lem 10220 zfac 10225 zfcndun 10380 zfcndac 10384 sup2 11940 supmul 11956 climmo 15275 summo 15438 prodmo 15655 gsumval3eu 19514 elpt 22732 bnj1185 32782 fineqvac 33075 satf0op 33348 sat1el2xp 33350 bj-bm1.3ii 35244 fdc 35912 sn-sup2 40446 cpcoll2d 41884 axc11next 42031 fnchoice 42579 ichexmpl1 44932 |
Copyright terms: Public domain | W3C validator |