Theorem cbvral 2722

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.)

Hypotheses

Ref	Expression
cbvral.1	|- F/ y ph
cbvral.2	|- F/ x ps
cbvral.3	|- ( x = y -> ( ph <-> ps ) )

Assertion

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

Distinct variable groups:   x, A   y, A

Allowed substitution hints:   ph( x, y)   ps( x, y)

Proof of Theorem cbvral

Step	Hyp	Ref	Expression
1		nfcv 2336	. 2 |- F/_ x A
2		nfcv 2336	. 2 |- F/_ y A
3		cbvral.1	. 2 |- F/ y ph
4		cbvral.2	. 2 |- F/ x ps
5		cbvral.3	. 2 |- ( x = y -> ( ph <-> ps ) )
6	1, 2, 3, 4, 5	cbvralf 2718	1 |- ( A. x e. A ph <-> A. y e. A ps )

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1471   A.wral 2472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477

This theorem is referenced by:  cbvralv  2726  cbvralsv  2742  cbviin  3950  frind  4383  ralxpf  4808  eqfnfv2f  5659  ralrnmpt  5700  dff13f  5813  ofrfval2  6147  uchoice  6190  fmpox  6253  cbvixp  6769  mptelixpg  6788  xpf1o  6900  indstr  9658  fsum3  11530  fsum00  11605  mertenslem2  11679  fprodcl2lem  11748  fprodle  11783  ctiunctal  12598  cnmpt11  14451  cnmpt21  14459  bj-bdfindes  15441  bj-findes  15473