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 ) ) |