Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017) (Revised by Gino Giotto, 10-Jan-2024) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbvaldvaw.1 | |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) |
|
| Assertion | cbvexdvaw | |- ( ph -> ( E. x ps <-> E. y ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvaldvaw.1 | |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) |
|
| 2 | 1 | notbid | |- ( ( ph /\ x = y ) -> ( -. ps <-> -. ch ) ) |
| 3 | 2 | cbvaldvaw | |- ( ph -> ( A. x -. ps <-> A. y -. ch ) ) |
| 4 | alnex | |- ( A. x -. ps <-> -. E. x ps ) |
|
| 5 | alnex | |- ( A. y -. ch <-> -. E. y ch ) |
|
| 6 | 3 4 5 | 3bitr3g | |- ( ph -> ( -. E. x ps <-> -. E. y ch ) ) |
| 7 | 6 | con4bid | |- ( ph -> ( E. x ps <-> E. y ch ) ) |