Metamath Proof Explorer

Theorem bnj1366

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1366.1 
|- ( ps <-> ( A e. _V /\ A. x e. A E! y ph /\ B = { y | E. x e. A ph } ) )
Assertion bnj1366 
|- ( ps -> B e. _V )

Proof

Step Hyp Ref Expression
1 bnj1366.1 
 |-  ( ps <-> ( A e. _V /\ A. x e. A E! y ph /\ B = { y | E. x e. A ph } ) )
2 1 simp3bi 
 |-  ( ps -> B = { y | E. x e. A ph } )
3 1 simp2bi 
 |-  ( ps -> A. x e. A E! y ph )
4 nfcv 
 |-  F/_ y A
5 nfeu1 
 |-  F/ y E! y ph
6 4 5 nfralw 
 |-  F/ y A. x e. A E! y ph
7 nfra1 
 |-  F/ x A. x e. A E! y ph
8 rspa 
 |-  ( ( A. x e. A E! y ph /\ x e. A ) -> E! y ph )
9 iota1 
 |-  ( E! y ph -> ( ph <-> ( iota y ph ) = y ) )
10 eqcom 
 |-  ( ( iota y ph ) = y <-> y = ( iota y ph ) )
11 9 10 bitrdi 
 |-  ( E! y ph -> ( ph <-> y = ( iota y ph ) ) )
12 8 11 syl 
 |-  ( ( A. x e. A E! y ph /\ x e. A ) -> ( ph <-> y = ( iota y ph ) ) )
13 7 12 rexbida 
 |-  ( A. x e. A E! y ph -> ( E. x e. A ph <-> E. x e. A y = ( iota y ph ) ) )
14 abid 
 |-  ( y e. { y | E. x e. A ph } <-> E. x e. A ph )
15 eqid 
 |-  ( x e. A |-> ( iota y ph ) ) = ( x e. A |-> ( iota y ph ) )
16 iotaex 
 |-  ( iota y ph ) e. _V
17 15 16 elrnmpti 
 |-  ( y e. ran ( x e. A |-> ( iota y ph ) ) <-> E. x e. A y = ( iota y ph ) )
18 13 14 17 3bitr4g 
 |-  ( A. x e. A E! y ph -> ( y e. { y | E. x e. A ph } <-> y e. ran ( x e. A |-> ( iota y ph ) ) ) )
19 6 18 alrimi 
 |-  ( A. x e. A E! y ph -> A. y ( y e. { y | E. x e. A ph } <-> y e. ran ( x e. A |-> ( iota y ph ) ) ) )
20 3 19 syl 
 |-  ( ps -> A. y ( y e. { y | E. x e. A ph } <-> y e. ran ( x e. A |-> ( iota y ph ) ) ) )
21 nfab1 
 |-  F/_ y { y | E. x e. A ph }
22 nfiota1 
 |-  F/_ y ( iota y ph )
23 4 22 nfmpt 
 |-  F/_ y ( x e. A |-> ( iota y ph ) )
24 23 nfrn 
 |-  F/_ y ran ( x e. A |-> ( iota y ph ) )
25 21 24 cleqf 
 |-  ( { y | E. x e. A ph } = ran ( x e. A |-> ( iota y ph ) ) <-> A. y ( y e. { y | E. x e. A ph } <-> y e. ran ( x e. A |-> ( iota y ph ) ) ) )
26 20 25 sylibr 
 |-  ( ps -> { y | E. x e. A ph } = ran ( x e. A |-> ( iota y ph ) ) )
27 2 26 eqtrd 
 |-  ( ps -> B = ran ( x e. A |-> ( iota y ph ) ) )
28 1 simp1bi 
 |-  ( ps -> A e. _V )
29 mptexg 
 |-  ( A e. _V -> ( x e. A |-> ( iota y ph ) ) e. _V )
30 rnexg 
 |-  ( ( x e. A |-> ( iota y ph ) ) e. _V -> ran ( x e. A |-> ( iota y ph ) ) e. _V )
31 28 29 30 3syl 
 |-  ( ps -> ran ( x e. A |-> ( iota y ph ) ) e. _V )
32 27 31 eqeltrd 
 |-  ( ps -> B e. _V )