# Metamath Proof Explorer

## Theorem ralab2

Description: Universal quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015) Drop ax-8 . (Revised by Gino Giotto, 1-Dec-2023)

Ref Expression
Hypothesis ralab2.1 ${⊢}{x}={y}\to \left({\psi }↔{\chi }\right)$
Assertion ralab2 ${⊢}\forall {x}\in \left\{{y}|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)$

### Proof

Step Hyp Ref Expression
1 ralab2.1 ${⊢}{x}={y}\to \left({\psi }↔{\chi }\right)$
2 df-ral ${⊢}\forall {x}\in \left\{{y}|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{y}|{\phi }\right\}\to {\psi }\right)$
3 nfsab1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{y}|{\phi }\right\}$
4 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
5 3 4 nfim ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{y}|{\phi }\right\}\to {\psi }\right)$
6 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)$
7 eleq1ab ${⊢}{x}={y}\to \left({x}\in \left\{{y}|{\phi }\right\}↔{y}\in \left\{{y}|{\phi }\right\}\right)$
8 abid ${⊢}{y}\in \left\{{y}|{\phi }\right\}↔{\phi }$
9 7 8 syl6bb ${⊢}{x}={y}\to \left({x}\in \left\{{y}|{\phi }\right\}↔{\phi }\right)$
10 9 1 imbi12d ${⊢}{x}={y}\to \left(\left({x}\in \left\{{y}|{\phi }\right\}\to {\psi }\right)↔\left({\phi }\to {\chi }\right)\right)$
11 5 6 10 cbvalv1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{y}|{\phi }\right\}\to {\psi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)$
12 2 11 bitri ${⊢}\forall {x}\in \left\{{y}|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)$