Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbvexv | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2006. (Revised by Wolf Lammen, 17-Jul-2021.) |
Ref | Expression |
---|---|
cbvalv.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvexv | ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvalv.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
2 | 1 | notbid 307 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
3 | 2 | cbvalv 2261 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
4 | 3 | notbii 309 | . 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓) |
5 | df-ex 1696 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
6 | df-ex 1696 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
7 | 4, 5, 6 | 3bitr4i 291 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∀wal 1473 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-nf 1701 |
This theorem is referenced by: cbvex2v 2275 eujust 2460 euind 3360 reuind 3378 cbvopab2v 4659 bm1.3ii 4712 reusv2lem2 4795 reusv2lem2OLD 4796 relop 5194 dmcoss 5306 fv3 6116 exfo 6285 zfun 6848 wfrlem1 7301 ac6sfi 8089 brwdom2 8361 aceq1 8823 aceq0 8824 aceq3lem 8826 dfac4 8828 kmlem2 8856 kmlem13 8867 axdc4lem 9160 zfac 9165 zfcndun 9316 zfcndac 9320 sup2 10858 supmul 10872 climmo 14136 summo 14295 prodmo 14505 gsumval3eu 18128 elpt 21185 usgraedg4 25916 bnj1185 30118 frrlem1 31024 fdc 32711 axc11next 37629 fnchoice 38211 |
Copyright terms: Public domain | W3C validator |