Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017) (Proof shortened by Wolf Lammen, 8-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvraldva2.1 | |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) |
|
| cbvraldva2.2 | |- ( ( ph /\ x = y ) -> A = B ) |
||
| Assertion | cbvrexdva2 | |- ( ph -> ( E. x e. A ps <-> E. y e. B ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvraldva2.1 | |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) |
|
| 2 | cbvraldva2.2 | |- ( ( ph /\ x = y ) -> A = B ) |
|
| 3 | 1 | notbid | |- ( ( ph /\ x = y ) -> ( -. ps <-> -. ch ) ) |
| 4 | 3 2 | cbvraldva2 | |- ( ph -> ( A. x e. A -. ps <-> A. y e. B -. ch ) ) |
| 5 | ralnex | |- ( A. x e. A -. ps <-> -. E. x e. A ps ) |
|
| 6 | ralnex | |- ( A. y e. B -. ch <-> -. E. y e. B ch ) |
|
| 7 | 4 5 6 | 3bitr3g | |- ( ph -> ( -. E. x e. A ps <-> -. E. y e. B ch ) ) |
| 8 | 7 | con4bid | |- ( ph -> ( E. x e. A ps <-> E. y e. B ch ) ) |