![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvexdvaw | Structured version Visualization version GIF version |
Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2413 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2375. (Revised by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024.) |
Ref | Expression |
---|---|
cbvaldvaw.1 | ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
cbvexdvaw | ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvaldvaw.1 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) | |
2 | 1 | notbid 318 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (¬ 𝜓 ↔ ¬ 𝜒)) |
3 | 2 | cbvaldvaw 2035 | . . 3 ⊢ (𝜑 → (∀𝑥 ¬ 𝜓 ↔ ∀𝑦 ¬ 𝜒)) |
4 | alnex 1778 | . . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓) | |
5 | alnex 1778 | . . 3 ⊢ (∀𝑦 ¬ 𝜒 ↔ ¬ ∃𝑦𝜒) | |
6 | 3, 4, 5 | 3bitr3g 313 | . 2 ⊢ (𝜑 → (¬ ∃𝑥𝜓 ↔ ¬ ∃𝑦𝜒)) |
7 | 6 | con4bid 317 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1535 ∃wex 1776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 |
This theorem is referenced by: cbvex2vw 2038 isinf 9294 isinfOLD 9295 cbvoprab123vw 36222 cbvoprab13vw 36224 cbveudavw 36234 cbvopab1davw 36247 cbvopab2davw 36248 cbvopabdavw 36249 cbvoprab1davw 36254 cbvoprab2davw 36255 cbvoprab3davw 36256 cbvoprab123davw 36257 cbvoprab12davw 36258 cbvoprab23davw 36259 cbvoprab13davw 36260 bj-gabeqis 36921 grumnud 44282 |
Copyright terms: Public domain | W3C validator |