# Metamath Proof Explorer

## Theorem dral2-o

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Version of dral2 using ax-c11 . (Contributed by NM, 27-Feb-2005) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis dral2-o.1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion dral2-o ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 dral2-o.1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 hbae-o ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
3 2 1 albidh ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\phantom{\rule{.4em}{0ex}}{\psi }\right)$