This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1468

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1468.1 
|- ( ps -> A. x ps )
bnj1468.2 
|- ( x = A -> ( ph <-> ps ) )
bnj1468.3 
|- ( y e. A -> A. x y e. A )
Assertion bnj1468 
|- ( A e. V -> ( [. A / x ]. ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 bnj1468.1 
 |-  ( ps -> A. x ps )
2 bnj1468.2 
 |-  ( x = A -> ( ph <-> ps ) )
3 bnj1468.3 
 |-  ( y e. A -> A. x y e. A )
4 sbccow 
 |-  ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )
5 ax-5 
 |-  ( ps -> A. y ps )
6 3 nfcii 
 |-  F/_ x A
7 6 nfeq2 
 |-  F/ x y = A
8 nfsbc1v 
 |-  F/ x [. y / x ]. ph
9 1 nf5i 
 |-  F/ x ps
10 8 9 nfbi 
 |-  F/ x ( [. y / x ]. ph <-> ps )
11 7 10 nfim 
 |-  F/ x ( y = A -> ( [. y / x ]. ph <-> ps ) )
12 11 nf5ri 
 |-  ( ( y = A -> ( [. y / x ]. ph <-> ps ) ) -> A. x ( y = A -> ( [. y / x ]. ph <-> ps ) ) )
13 ax6ev 
 |-  E. x x = y
14 eqeq1 
 |-  ( x = y -> ( x = A <-> y = A ) )
15 14 2 biimtrrdi 
 |-  ( x = y -> ( y = A -> ( ph <-> ps ) ) )
16 sbceq1a 
 |-  ( x = y -> ( ph <-> [. y / x ]. ph ) )
17 16 bibi1d 
 |-  ( x = y -> ( ( ph <-> ps ) <-> ( [. y / x ]. ph <-> ps ) ) )
18 15 17 sylibd 
 |-  ( x = y -> ( y = A -> ( [. y / x ]. ph <-> ps ) ) )
19 13 18 bnj101 
 |-  E. x ( y = A -> ( [. y / x ]. ph <-> ps ) )
20 12 19 bnj1131 
 |-  ( y = A -> ( [. y / x ]. ph <-> ps ) )
21 5 20 bnj1464 
 |-  ( A e. V -> ( [. A / y ]. [. y / x ]. ph <-> ps ) )
22 4 21 bitr3id 
 |-  ( A e. V -> ( [. A / x ]. ph <-> ps ) )