Metamath Proof Explorer

Theorem reu6f

Description: Version of reu6 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BTernaryTau, 29-Sep-2026)

Ref Expression
Hypothesis reu6f.1 
|- F/ y ph
Assertion reu6f 
|- ( E! x e. A ph <-> E. y e. A A. x e. A ( ph <-> x = y ) )

Proof

Step Hyp Ref Expression
1 reu6f.1 
 |-  F/ y ph
2 df-reu 
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
3 19.28v 
 |-  ( A. x ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) <-> ( y e. A /\ A. x ( x e. A -> ( ph <-> x = y ) ) ) )
4 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
5 sbequ12 
 |-  ( x = y -> ( ph <-> [ y / x ] ph ) )
6 4 5 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ [ y / x ] ph ) ) )
7 equequ1 
 |-  ( x = y -> ( x = y <-> y = y ) )
8 6 7 bibi12d 
 |-  ( x = y -> ( ( ( x e. A /\ ph ) <-> x = y ) <-> ( ( y e. A /\ [ y / x ] ph ) <-> y = y ) ) )
9 equid 
 |-  y = y
10 9 tbt 
 |-  ( ( y e. A /\ [ y / x ] ph ) <-> ( ( y e. A /\ [ y / x ] ph ) <-> y = y ) )
11 simpl 
 |-  ( ( y e. A /\ [ y / x ] ph ) -> y e. A )
12 10 11 sylbir 
 |-  ( ( ( y e. A /\ [ y / x ] ph ) <-> y = y ) -> y e. A )
13 8 12 biimtrdi 
 |-  ( x = y -> ( ( ( x e. A /\ ph ) <-> x = y ) -> y e. A ) )
14 13 spimvw 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) -> y e. A )
15 ibar 
 |-  ( x e. A -> ( ph <-> ( x e. A /\ ph ) ) )
16 15 bibi1d 
 |-  ( x e. A -> ( ( ph <-> x = y ) <-> ( ( x e. A /\ ph ) <-> x = y ) ) )
17 16 biimprcd 
 |-  ( ( ( x e. A /\ ph ) <-> x = y ) -> ( x e. A -> ( ph <-> x = y ) ) )
18 17 sps 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) -> ( x e. A -> ( ph <-> x = y ) ) )
19 14 18 jca 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) -> ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) )
20 19 axc4i 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) -> A. x ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) )
21 biimp 
 |-  ( ( ph <-> x = y ) -> ( ph -> x = y ) )
22 21 imim2i 
 |-  ( ( x e. A -> ( ph <-> x = y ) ) -> ( x e. A -> ( ph -> x = y ) ) )
23 22 impd 
 |-  ( ( x e. A -> ( ph <-> x = y ) ) -> ( ( x e. A /\ ph ) -> x = y ) )
24 23 adantl 
 |-  ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> ( ( x e. A /\ ph ) -> x = y ) )
25 4 biimprcd 
 |-  ( y e. A -> ( x = y -> x e. A ) )
26 25 adantr 
 |-  ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> ( x = y -> x e. A ) )
27 26 imp 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> x e. A )
28 simplr 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> ( x e. A -> ( ph <-> x = y ) ) )
29 simpr 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> x = y )
30 biimpr 
 |-  ( ( ph <-> x = y ) -> ( x = y -> ph ) )
31 28 29 30 syl6ci 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> ( x e. A -> ph ) )
32 27 31 jcai 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> ( x e. A /\ ph ) )
33 32 ex 
 |-  ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> ( x = y -> ( x e. A /\ ph ) ) )
34 24 33 impbid 
 |-  ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> ( ( x e. A /\ ph ) <-> x = y ) )
35 34 alimi 
 |-  ( A. x ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> A. x ( ( x e. A /\ ph ) <-> x = y ) )
36 20 35 impbii 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) <-> A. x ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) )
37 df-ral 
 |-  ( A. x e. A ( ph <-> x = y ) <-> A. x ( x e. A -> ( ph <-> x = y ) ) )
38 37 anbi2i 
 |-  ( ( y e. A /\ A. x e. A ( ph <-> x = y ) ) <-> ( y e. A /\ A. x ( x e. A -> ( ph <-> x = y ) ) ) )
39 3 36 38 3bitr4i 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) <-> ( y e. A /\ A. x e. A ( ph <-> x = y ) ) )
40 39 exbii 
 |-  ( E. y A. x ( ( x e. A /\ ph ) <-> x = y ) <-> E. y ( y e. A /\ A. x e. A ( ph <-> x = y ) ) )
41 nfv 
 |-  F/ y x e. A
42 41 1 nfan 
 |-  F/ y ( x e. A /\ ph )
43 42 euf 
 |-  ( E! x ( x e. A /\ ph ) <-> E. y A. x ( ( x e. A /\ ph ) <-> x = y ) )
44 df-rex 
 |-  ( E. y e. A A. x e. A ( ph <-> x = y ) <-> E. y ( y e. A /\ A. x e. A ( ph <-> x = y ) ) )
45 40 43 44 3bitr4i 
 |-  ( E! x ( x e. A /\ ph ) <-> E. y e. A A. x e. A ( ph <-> x = y ) )
46 2 45 bitri 
 |-  ( E! x e. A ph <-> E. y e. A A. x e. A ( ph <-> x = y ) )