Theorem cbvral 1796

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 970	. 2 |- (z e. A -> A.x z e. A)
2		ax-17 970	. 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 1795	1 |- (A.x e. A ph <-> A.y e. A ps)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 953   = wceq 955   e. wcel 957  A.wral 1644

This theorem is referenced by:  cbvralv 1798  sbralie 1939  cbvralsv 1965  tfinds 3158  tfindes 3161  ralxpf 3217  eqfnfvf 3795  f1fvf 3872  tfrlem1 3908  uniimadomf 4798  isumnn0nna 7179  isummulc1a 7185  isumcmpi 7186  fsum0diag4 7232

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-ext 1459

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

Copyright terms: Public domain