| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simpr |
|- ( ( .~ Er A /\ z e. A ) -> z e. A ) |
| 2 |
|
simpl |
|- ( ( .~ Er A /\ z e. A ) -> .~ Er A ) |
| 3 |
2 1
|
erref |
|- ( ( .~ Er A /\ z e. A ) -> z .~ z ) |
| 4 |
|
breq1 |
|- ( v = z -> ( v .~ z <-> z .~ z ) ) |
| 5 |
|
breq1 |
|- ( v = z -> ( v .~ w <-> z .~ w ) ) |
| 6 |
4 5
|
anbi12d |
|- ( v = z -> ( ( v .~ z /\ v .~ w ) <-> ( z .~ z /\ z .~ w ) ) ) |
| 7 |
6
|
rspcev |
|- ( ( z e. A /\ ( z .~ z /\ z .~ w ) ) -> E. v e. A ( v .~ z /\ v .~ w ) ) |
| 8 |
7
|
expr |
|- ( ( z e. A /\ z .~ z ) -> ( z .~ w -> E. v e. A ( v .~ z /\ v .~ w ) ) ) |
| 9 |
1 3 8
|
syl2anc |
|- ( ( .~ Er A /\ z e. A ) -> ( z .~ w -> E. v e. A ( v .~ z /\ v .~ w ) ) ) |
| 10 |
|
simplll |
|- ( ( ( ( .~ Er A /\ z e. A ) /\ v e. A ) /\ ( v .~ z /\ v .~ w ) ) -> .~ Er A ) |
| 11 |
|
simprl |
|- ( ( ( ( .~ Er A /\ z e. A ) /\ v e. A ) /\ ( v .~ z /\ v .~ w ) ) -> v .~ z ) |
| 12 |
|
simprr |
|- ( ( ( ( .~ Er A /\ z e. A ) /\ v e. A ) /\ ( v .~ z /\ v .~ w ) ) -> v .~ w ) |
| 13 |
10 11 12
|
ertr3d |
|- ( ( ( ( .~ Er A /\ z e. A ) /\ v e. A ) /\ ( v .~ z /\ v .~ w ) ) -> z .~ w ) |
| 14 |
13
|
rexlimdva2 |
|- ( ( .~ Er A /\ z e. A ) -> ( E. v e. A ( v .~ z /\ v .~ w ) -> z .~ w ) ) |
| 15 |
9 14
|
impbid |
|- ( ( .~ Er A /\ z e. A ) -> ( z .~ w <-> E. v e. A ( v .~ z /\ v .~ w ) ) ) |
| 16 |
|
vex |
|- z e. _V |
| 17 |
|
vex |
|- v e. _V |
| 18 |
16 17
|
elec |
|- ( z e. [ v ] .~ <-> v .~ z ) |
| 19 |
|
vex |
|- w e. _V |
| 20 |
19 17
|
elec |
|- ( w e. [ v ] .~ <-> v .~ w ) |
| 21 |
18 20
|
anbi12i |
|- ( ( z e. [ v ] .~ /\ w e. [ v ] .~ ) <-> ( v .~ z /\ v .~ w ) ) |
| 22 |
21
|
rexbii |
|- ( E. v e. A ( z e. [ v ] .~ /\ w e. [ v ] .~ ) <-> E. v e. A ( v .~ z /\ v .~ w ) ) |
| 23 |
15 22
|
bitr4di |
|- ( ( .~ Er A /\ z e. A ) -> ( z .~ w <-> E. v e. A ( z e. [ v ] .~ /\ w e. [ v ] .~ ) ) ) |
| 24 |
23
|
ex |
|- ( .~ Er A -> ( z e. A -> ( z .~ w <-> E. v e. A ( z e. [ v ] .~ /\ w e. [ v ] .~ ) ) ) ) |