Theorem cbvral 1798

Description: Rule used to change bound variables with implicit substitution.

Hypotheses

Ref	Expression
cbvral.1	|- (ph -> A.yph)
cbvral.2	|- (ps -> A.xps)
cbvral.3	|- (x = y -> (ph <-> ps))

Assertion

Ref	Expression
cbvral	|- (A.x e. A ph <-> A.y e. A ps)

Distinct variable group:   x,y,A

Proof of Theorem cbvral

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (z e. A -> A.x z e. A)
2		ax-17 971	. 2 |- (z e. A -> A.y z e. A)
3		cbvral.1	. 2 |- (ph -> A.yph)
4		cbvral.2	. 2 |- (ps -> A.xps)
5		cbvral.3	. 2 |- (x = y -> (ph <-> ps))
6	1, 2, 3, 4, 5	cbvralf 1796	1 |- (A.x e. A ph <-> A.y e. A ps)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   = wceq 956   e. wcel 958  A.wral 1645

This theorem is referenced by:  cbvralv 1800  sbralie 1941  cbvralsv 1967  tfinds 3161  tfindes 3164  ralxpf 3220  eqfnfvf 3798  f1fvf 3875  tfrlem1 3911  uniimadomf 4811  isumnn0nna 7208  isummulc1a 7214  isumcmpi 7215  fsum0diag4 7261

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472  df-ral 1649

Copyright terms: Public domain