Metamath Proof Explorer


Theorem bnj89

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

Ref Expression
Hypothesis bnj89.1 Z V
Assertion bnj89 [˙Z / y]˙ ∃! x φ ∃! x [˙Z / y]˙ φ

Proof

Step Hyp Ref Expression
1 bnj89.1 Z V
2 sbcex2 [˙Z / y]˙ w x φ x = w w [˙Z / y]˙ x φ x = w
3 sbcal [˙Z / y]˙ x φ x = w x [˙Z / y]˙ φ x = w
4 3 exbii w [˙Z / y]˙ x φ x = w w x [˙Z / y]˙ φ x = w
5 sbcbig Z V [˙Z / y]˙ φ x = w [˙Z / y]˙ φ [˙Z / y]˙ x = w
6 1 5 ax-mp [˙Z / y]˙ φ x = w [˙Z / y]˙ φ [˙Z / y]˙ x = w
7 sbcg Z V [˙Z / y]˙ x = w x = w
8 1 7 ax-mp [˙Z / y]˙ x = w x = w
9 8 bibi2i [˙Z / y]˙ φ [˙Z / y]˙ x = w [˙Z / y]˙ φ x = w
10 6 9 bitri [˙Z / y]˙ φ x = w [˙Z / y]˙ φ x = w
11 10 albii x [˙Z / y]˙ φ x = w x [˙Z / y]˙ φ x = w
12 11 exbii w x [˙Z / y]˙ φ x = w w x [˙Z / y]˙ φ x = w
13 2 4 12 3bitri [˙Z / y]˙ w x φ x = w w x [˙Z / y]˙ φ x = w
14 eu6 ∃! x φ w x φ x = w
15 14 sbcbii [˙Z / y]˙ ∃! x φ [˙Z / y]˙ w x φ x = w
16 eu6 ∃! x [˙Z / y]˙ φ w x [˙Z / y]˙ φ x = w
17 13 15 16 3bitr4i [˙Z / y]˙ ∃! x φ ∃! x [˙Z / y]˙ φ