Theorem cbvral 3306

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

Hypotheses

Ref	Expression
cbvral.1	⊢ Ⅎ𝑦𝜑
cbvral.2	⊢ Ⅎ𝑥𝜓
cbvral.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvral	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvral

Step	Hyp	Ref	Expression
1		nfcv 2902	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2902	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvral.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvral.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvral.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvralf 3304	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1857  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clel 2756  df-nfc 2891  df-ral 3055

This theorem is referenced by:  cbvralv  3310  cbvralsv  3321  cbviin  4710  disjxun  4802  ralxpf  5424  eqfnfv2f  6479  ralrnmpt  6532  dff13f  6677  ofrfval2  7081  fmpt2x  7405  ovmptss  7427  cbvixp  8093  mptelixpg  8113  boxcutc  8119  xpf1o  8289  indexfi  8441  ixpiunwdom  8663  dfac8clem  9065  acni2  9079  ac6num  9513  ac6c4  9515  iundom2g  9574  uniimadomf  9579  rabssnn0fi  12999  rlim2  14446  ello1mpt  14471  o1compt  14537  fsum00  14749  iserodd  15762  pcmptdvds  15820  catpropd  16590  invfuc  16855  gsummptnn0fz  18602  gsummoncoe1  19896  gsumply1eq  19897  fiuncmp  21429  elptr2  21599  ptcld  21638  ptclsg  21640  ptcnplem  21646  cnmpt11  21688  cnmpt21  21696  ovoliunlem3  23492  ovoliun  23493  ovoliun2  23494  finiunmbl  23532  volfiniun  23535  iunmbl  23541  voliun  23542  mbfeqalem  23628  mbfsup  23650  mbfinf  23651  mbflim  23654  itg2split  23735  itgeqa  23799  itgfsum  23812  itgabs  23820  itggt0  23827  limciun  23877  dvlipcn  23976  dvfsumlem4  24011  dvfsum2  24016  itgsubst  24031  coeeq2  24217  ulmss  24370  leibpi  24889  rlimcnp  24912  o1cxp  24921  lgamgulmlem6  24980  fsumdvdscom  25131  lgseisenlem2  25321  disjunsn  29735  bnj110  31256  bnj1529  31466  poimirlem23  33763  itgabsnc  33810  itggt0cn  33813  totbndbnd  33919  disjinfi  39897  fmptf  39965  climinff  40364  idlimc  40379  fnlimabslt  40432  limsupref  40438  limsupbnd1f  40439  climbddf  40440  climinf2  40460  limsupubuz  40466  climinfmpt  40468  limsupmnf  40474  limsupre2  40478  limsupmnfuz  40480  limsupre3  40486  limsupre3uz  40489  limsupreuz  40490  climuz  40497  lmbr3  40500  liminflelimsup  40529  limsupgt  40531  liminfreuz  40556  liminflt  40558  xlimmnf  40588  xlimpnf  40589  dfxlim2  40595  cncfshift  40608  stoweidlem31  40769  iundjiun  41198  meaiunincf  41221  pimgtmnf2  41448  smfpimcc  41538  smfsup  41544  smfinflem  41547  smfinf  41548  cbvral2  41696