Metamath Proof Explorer

Theorem bj-axreprepsep

Description: Strong axiom of replacement (universal closure of ax-rep ) from the axioms of separation and replacement as written in the theorem's hypotheses.

The statement does not require a nonempty universe; most of the proof does not either, except for the use of 19.8a , which could be removed by reworking the proof, since it is applied in a subexpression bound by the variable it introduces. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv . (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-axreprepsep.axsep 
|- A. x E. s A. y ( y e. s <-> ( y e. x /\ E. z ph ) )
bj-axreprepsep.axrep 
|- A. s ( A. y e. s E! z ph -> E. t A. z ( z e. t <-> E. y e. s ph ) )
Assertion bj-axreprepsep 
|- A. x ( A. y e. x E* z ph -> E. t A. z ( z e. t <-> E. y e. x ph ) )

Proof

Step Hyp Ref Expression
1 bj-axreprepsep.axsep 
 |-  A. x E. s A. y ( y e. s <-> ( y e. x /\ E. z ph ) )
2 bj-axreprepsep.axrep 
 |-  A. s ( A. y e. s E! z ph -> E. t A. z ( z e. t <-> E. y e. s ph ) )
3 19.42v 
 |-  ( E. s ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) <-> ( A. y e. x E* z ph /\ E. s A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) )
4 bianir 
 |-  ( ( E. t A. z ( z e. t <-> E. y e. s ph ) /\ ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) ) -> E. t A. z ( z e. t <-> E. y e. x ph ) )
5 4 ax-gen 
 |-  A. s ( ( E. t A. z ( z e. t <-> E. y e. s ph ) /\ ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) ) -> E. t A. z ( z e. t <-> E. y e. x ph ) )
6 pm3.43 
 |-  ( ( ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. t A. z ( z e. t <-> E. y e. s ph ) ) /\ ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) ) ) -> ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> ( E. t A. z ( z e. t <-> E. y e. s ph ) /\ ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) ) ) )
7 df-ral 
 |-  ( A. y e. x E* z ph <-> A. y ( y e. x -> E* z ph ) )
8 bicom1 
 |-  ( ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( ( y e. x /\ E. z ph ) <-> y e. s ) )
9 8 biimprcd 
 |-  ( y e. s -> ( ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( y e. x /\ E. z ph ) ) )
10 df-eu 
 |-  ( E! z ph <-> ( E. z ph /\ E* z ph ) )
11 10 simplbi2com 
 |-  ( E* z ph -> ( E. z ph -> E! z ph ) )
12 11 imim2i 
 |-  ( ( y e. x -> E* z ph ) -> ( y e. x -> ( E. z ph -> E! z ph ) ) )
13 12 impd 
 |-  ( ( y e. x -> E* z ph ) -> ( ( y e. x /\ E. z ph ) -> E! z ph ) )
14 13 com12 
 |-  ( ( y e. x /\ E. z ph ) -> ( ( y e. x -> E* z ph ) -> E! z ph ) )
15 9 14 syl6 
 |-  ( y e. s -> ( ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( ( y e. x -> E* z ph ) -> E! z ph ) ) )
16 15 impd 
 |-  ( y e. s -> ( ( ( y e. s <-> ( y e. x /\ E. z ph ) ) /\ ( y e. x -> E* z ph ) ) -> E! z ph ) )
17 16 com12 
 |-  ( ( ( y e. s <-> ( y e. x /\ E. z ph ) ) /\ ( y e. x -> E* z ph ) ) -> ( y e. s -> E! z ph ) )
18 17 ancoms 
 |-  ( ( ( y e. x -> E* z ph ) /\ ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> ( y e. s -> E! z ph ) )
19 18 alanimi 
 |-  ( ( A. y ( y e. x -> E* z ph ) /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> A. y ( y e. s -> E! z ph ) )
20 7 19 sylanb 
 |-  ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> A. y ( y e. s -> E! z ph ) )
21 20 ralrid 
 |-  ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> A. y e. s E! z ph )
22 21 ax-gen 
 |-  A. s ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> A. y e. s E! z ph )
23 2 22 barbara 
 |-  A. s ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. t A. z ( z e. t <-> E. y e. s ph ) )
24 nfv 
 |-  F/ z y e. s
25 nfv 
 |-  F/ z y e. x
26 nfe1 
 |-  F/ z E. z ph
27 25 26 nfan 
 |-  F/ z ( y e. x /\ E. z ph )
28 24 27 nfbi 
 |-  F/ z ( y e. s <-> ( y e. x /\ E. z ph ) )
29 28 nfal 
 |-  F/ z A. y ( y e. s <-> ( y e. x /\ E. z ph ) )
30 19.8a 
 |-  ( ph -> E. z ph )
31 biimpr 
 |-  ( ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( ( y e. x /\ E. z ph ) -> y e. s ) )
32 30 31 sylan2i 
 |-  ( ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( ( y e. x /\ ph ) -> y e. s ) )
33 simpr 
 |-  ( ( y e. x /\ ph ) -> ph )
34 32 33 jca2 
 |-  ( ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( ( y e. x /\ ph ) -> ( y e. s /\ ph ) ) )
35 bj-bisimpl 
 |-  ( ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( y e. s -> y e. x ) )
36 35 anim1d 
 |-  ( ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( ( y e. s /\ ph ) -> ( y e. x /\ ph ) ) )
37 34 36 impbid 
 |-  ( ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( ( y e. x /\ ph ) <-> ( y e. s /\ ph ) ) )
38 37 alexbii 
 |-  ( A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( E. y ( y e. x /\ ph ) <-> E. y ( y e. s /\ ph ) ) )
39 df-rex 
 |-  ( E. y e. x ph <-> E. y ( y e. x /\ ph ) )
40 df-rex 
 |-  ( E. y e. s ph <-> E. y ( y e. s /\ ph ) )
41 38 39 40 3bitr4g 
 |-  ( A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( E. y e. x ph <-> E. y e. s ph ) )
42 41 bibi2d 
 |-  ( A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( ( z e. t <-> E. y e. x ph ) <-> ( z e. t <-> E. y e. s ph ) ) )
43 29 42 albid 
 |-  ( A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( A. z ( z e. t <-> E. y e. x ph ) <-> A. z ( z e. t <-> E. y e. s ph ) ) )
44 43 exbidv 
 |-  ( A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) -> ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) )
45 44 adantl 
 |-  ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) )
46 45 ax-gen 
 |-  A. s ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) )
47 19.26 
 |-  ( A. s ( ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. t A. z ( z e. t <-> E. y e. s ph ) ) /\ ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) ) ) <-> ( A. s ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. t A. z ( z e. t <-> E. y e. s ph ) ) /\ A. s ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) ) ) )
48 23 46 47 mpbir2an 
 |-  A. s ( ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. t A. z ( z e. t <-> E. y e. s ph ) ) /\ ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) ) )
49 6 48 bj-alimii 
 |-  A. s ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> ( E. t A. z ( z e. t <-> E. y e. s ph ) /\ ( E. t A. z ( z e. t <-> E. y e. x ph ) <-> E. t A. z ( z e. t <-> E. y e. s ph ) ) ) )
50 5 49 barbara 
 |-  A. s ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. t A. z ( z e. t <-> E. y e. x ph ) )
51 exim 
 |-  ( A. s ( ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. t A. z ( z e. t <-> E. y e. x ph ) ) -> ( E. s ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. s E. t A. z ( z e. t <-> E. y e. x ph ) ) )
52 50 51 ax-mp 
 |-  ( E. s ( A. y e. x E* z ph /\ A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. s E. t A. z ( z e. t <-> E. y e. x ph ) )
53 3 52 sylbir 
 |-  ( ( A. y e. x E* z ph /\ E. s A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) ) -> E. s E. t A. z ( z e. t <-> E. y e. x ph ) )
54 53 ex 
 |-  ( A. y e. x E* z ph -> ( E. s A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) -> E. s E. t A. z ( z e. t <-> E. y e. x ph ) ) )
55 ax5e 
 |-  ( E. s E. t A. z ( z e. t <-> E. y e. x ph ) -> E. t A. z ( z e. t <-> E. y e. x ph ) )
56 54 55 syl6 
 |-  ( A. y e. x E* z ph -> ( E. s A. y ( y e. s <-> ( y e. x /\ E. z ph ) ) -> E. t A. z ( z e. t <-> E. y e. x ph ) ) )
57 56 1 bj-almpig 
 |-  A. x ( A. y e. x E* z ph -> E. t A. z ( z e. t <-> E. y e. x ph ) )