|   | 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 2414 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2376. (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 2036 | . . 3 ⊢ (𝜑 → (∀𝑥 ¬ 𝜓 ↔ ∀𝑦 ¬ 𝜒)) | 
| 4 | alnex 1780 | . . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓) | |
| 5 | alnex 1780 | . . 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 1537 ∃wex 1778 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 | 
| This theorem is referenced by: cbvex2vw 2039 isinf 9297 isinfOLD 9298 cbvoprab123vw 36241 cbvoprab13vw 36243 cbveudavw 36253 cbvopab1davw 36266 cbvopab2davw 36267 cbvopabdavw 36268 cbvoprab1davw 36273 cbvoprab2davw 36274 cbvoprab3davw 36275 cbvoprab123davw 36276 cbvoprab12davw 36277 cbvoprab23davw 36278 cbvoprab13davw 36279 bj-gabeqis 36940 grumnud 44310 | 
| Copyright terms: Public domain | W3C validator |