# Metamath Proof Explorer

## Theorem cbvrexfw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf with a disjoint variable condition, which does not require ax-13 . (Contributed by FL, 27-Apr-2008) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvrexfw.1
`|- F/_ x A`
cbvrexfw.2
`|- F/_ y A`
cbvrexfw.3
`|- F/ y ph`
cbvrexfw.4
`|- F/ x ps`
cbvrexfw.5
`|- ( x = y -> ( ph <-> ps ) )`
Assertion cbvrexfw
`|- ( E. x e. A ph <-> E. y e. A ps )`

### Proof

Step Hyp Ref Expression
1 cbvrexfw.1
` |-  F/_ x A`
2 cbvrexfw.2
` |-  F/_ y A`
3 cbvrexfw.3
` |-  F/ y ph`
4 cbvrexfw.4
` |-  F/ x ps`
5 cbvrexfw.5
` |-  ( x = y -> ( ph <-> ps ) )`
6 3 nfn
` |-  F/ y -. ph`
7 4 nfn
` |-  F/ x -. ps`
8 5 notbid
` |-  ( x = y -> ( -. ph <-> -. ps ) )`
9 1 2 6 7 8 cbvralfw
` |-  ( A. x e. A -. ph <-> A. y e. A -. ps )`
10 9 notbii
` |-  ( -. A. x e. A -. ph <-> -. A. y e. A -. ps )`
11 dfrex2
` |-  ( E. x e. A ph <-> -. A. x e. A -. ph )`
12 dfrex2
` |-  ( E. y e. A ps <-> -. A. y e. A -. ps )`
13 10 11 12 3bitr4i
` |-  ( E. x e. A ph <-> E. y e. A ps )`