# Metamath Proof Explorer

## Theorem cbvral2vw

Description: Version of cbvral2v with a disjoint variable condition, which does not require ax-13 . (Contributed by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvral2vw.1 ${⊢}{x}={z}\to \left({\phi }↔{\chi }\right)$
cbvral2vw.2 ${⊢}{y}={w}\to \left({\chi }↔{\psi }\right)$
Assertion cbvral2vw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 cbvral2vw.1 ${⊢}{x}={z}\to \left({\phi }↔{\chi }\right)$
2 cbvral2vw.2 ${⊢}{y}={w}\to \left({\chi }↔{\psi }\right)$
3 1 ralbidv ${⊢}{x}={z}\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 3 cbvralvw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }$
5 2 cbvralvw ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }↔\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
6 5 ralbii ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
7 4 6 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$