Metamath Proof Explorer

Theorem alxfr

Description: Transfer universal quantification from a variable x to another variable y contained in expression A . (Contributed by NM, 18-Feb-2007)

Ref Expression
Hypothesis alxfr.1 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
Assertion alxfr ${⊢}\left(\forall {y}\phantom{\rule{.4em}{0ex}}{A}\in {B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{x}={A}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

Proof

Step Hyp Ref Expression
1 alxfr.1 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
2 1 spcgv ${⊢}{A}\in {B}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)$
3 2 com12 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({A}\in {B}\to {\psi }\right)$
4 3 alimdv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}{A}\in {B}\to \forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
5 4 com12 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{A}\in {B}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
6 5 adantr ${⊢}\left(\forall {y}\phantom{\rule{.4em}{0ex}}{A}\in {B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{x}={A}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
7 nfa1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
8 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
9 sp ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to {\psi }$
10 9 1 syl5ibrcom ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \left({x}={A}\to {\phi }\right)$
11 7 8 10 exlimd ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}={A}\to {\phi }\right)$
12 11 alimdv ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{x}={A}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
13 12 com12 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{x}={A}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
14 13 adantl ${⊢}\left(\forall {y}\phantom{\rule{.4em}{0ex}}{A}\in {B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{x}={A}\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
15 6 14 impbid ${⊢}\left(\forall {y}\phantom{\rule{.4em}{0ex}}{A}\in {B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{x}={A}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$