# Metamath Proof Explorer

## Theorem bnj1209

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1209.1 ${⊢}{\chi }\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
bnj1209.2 ${⊢}{\theta }↔\left({\chi }\wedge {x}\in {B}\wedge {\phi }\right)$
Assertion bnj1209 ${⊢}{\chi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\theta }$

### Proof

Step Hyp Ref Expression
1 bnj1209.1 ${⊢}{\chi }\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
2 bnj1209.2 ${⊢}{\theta }↔\left({\chi }\wedge {x}\in {B}\wedge {\phi }\right)$
3 1 bnj1196 ${⊢}{\chi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {\phi }\right)$
4 3 ancli ${⊢}{\chi }\to \left({\chi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {\phi }\right)\right)$
5 19.42v ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge \left({x}\in {B}\wedge {\phi }\right)\right)↔\left({\chi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {\phi }\right)\right)$
6 4 5 sylibr ${⊢}{\chi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge \left({x}\in {B}\wedge {\phi }\right)\right)$
7 3anass ${⊢}\left({\chi }\wedge {x}\in {B}\wedge {\phi }\right)↔\left({\chi }\wedge \left({x}\in {B}\wedge {\phi }\right)\right)$
8 2 7 bitri ${⊢}{\theta }↔\left({\chi }\wedge \left({x}\in {B}\wedge {\phi }\right)\right)$
9 6 8 bnj1198 ${⊢}{\chi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\theta }$