Metamath Proof Explorer

Theorem bm1.3ii

Description: Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep . Similar to Theorem 1.3(ii) of BellMachover p. 463. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis bm1.3ii.1 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {x}\right)$
Assertion bm1.3ii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{\phi }\right)$

Proof

Step Hyp Ref Expression
1 bm1.3ii.1 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {x}\right)$
2 19.42v ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {z}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {z}\wedge {\phi }\right)\right)\right)↔\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {z}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {z}\wedge {\phi }\right)\right)\right)$
3 bimsc1 ${⊢}\left(\left({\phi }\to {y}\in {z}\right)\wedge \left({y}\in {x}↔\left({y}\in {z}\wedge {\phi }\right)\right)\right)\to \left({y}\in {x}↔{\phi }\right)$
4 3 alanimi ${⊢}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {z}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {z}\wedge {\phi }\right)\right)\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{\phi }\right)$
5 4 eximi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {z}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {z}\wedge {\phi }\right)\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{\phi }\right)$
6 2 5 sylbir ${⊢}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {z}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {z}\wedge {\phi }\right)\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{\phi }\right)$
7 elequ2 ${⊢}{x}={z}\to \left({y}\in {x}↔{y}\in {z}\right)$
8 7 imbi2d ${⊢}{x}={z}\to \left(\left({\phi }\to {y}\in {x}\right)↔\left({\phi }\to {y}\in {z}\right)\right)$
9 8 albidv ${⊢}{x}={z}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {x}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {z}\right)\right)$
10 9 cbvexvw ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {x}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {z}\right)$
11 1 10 mpbi ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {z}\right)$
12 ax-sep ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {z}\wedge {\phi }\right)\right)$
13 11 12 exan ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}\in {z}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {z}\wedge {\phi }\right)\right)\right)$
14 6 13 exlimiiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{\phi }\right)$