Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
cbvrexfw
Metamath Proof Explorer
Description: Rule used to change bound variables, using implicit substitution.
Version of cbvrexf with a disjoint variable condition, which does not
require ax-13 . For a version not dependent on ax-11 and ax-12, see
cbvrexvw . (Contributed by FL , 27-Apr-2008) Avoid ax-10 ,
ax-13 . (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
ralnex
|- ( A. x e. A -. ph <-> -. E. x e. A ph )
11
ralnex
|- ( A. y e. A -. ps <-> -. E. y e. A ps )
12
9 10 11
3bitr3i
|- ( -. E. x e. A ph <-> -. E. y e. A ps )
13
12
con4bii
|- ( E. x e. A ph <-> E. y e. A ps )