Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
cbvralfw
Metamath Proof Explorer
Description: Rule used to change bound variables, using implicit substitution.
Version of cbvralf with a disjoint variable condition, which does not
require ax-10 , ax-13 . For a version not dependent on ax-11 and
ax-12, see cbvralvw . (Contributed by NM , 7-Mar-2004) Avoid
ax-10 , ax-13 . (Revised by Gino Giotto , 23-May-2024)
Ref
Expression
Hypotheses
cbvralfw.1
|- F/_ x A
cbvralfw.2
|- F/_ y A
cbvralfw.3
|- F/ y ph
cbvralfw.4
|- F/ x ps
cbvralfw.5
|- ( x = y -> ( ph <-> ps ) )
Assertion
cbvralfw
|- ( A. x e. A ph <-> A. y e. A ps )
Proof
Step
Hyp
Ref
Expression
1
cbvralfw.1
|- F/_ x A
2
cbvralfw.2
|- F/_ y A
3
cbvralfw.3
|- F/ y ph
4
cbvralfw.4
|- F/ x ps
5
cbvralfw.5
|- ( x = y -> ( ph <-> ps ) )
6
2
nfcri
|- F/ y x e. A
7
6 3
nfim
|- F/ y ( x e. A -> ph )
8
1
nfcri
|- F/ x y e. A
9
8 4
nfim
|- F/ x ( y e. A -> ps )
10
eleq1w
|- ( x = y -> ( x e. A <-> y e. A ) )
11
10 5
imbi12d
|- ( x = y -> ( ( x e. A -> ph ) <-> ( y e. A -> ps ) ) )
12
7 9 11
cbvalv1
|- ( A. x ( x e. A -> ph ) <-> A. y ( y e. A -> ps ) )
13
df-ral
|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
14
df-ral
|- ( A. y e. A ps <-> A. y ( y e. A -> ps ) )
15
12 13 14
3bitr4i
|- ( A. x e. A ph <-> A. y e. A ps )