Theorem cbvral 3363

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 2934	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2934	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvral.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvral.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvral.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvralf 3361	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 198  Ⅎwnf 1827  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clel 2774  df-nfc 2921  df-ral 3095

This theorem is referenced by:  cbvralv  3367  cbvralsv  3378  cbviin  4793  disjxun  4886  ralxpf  5516  eqfnfv2f  6580  ralrnmpt  6634  dff13f  6787  ofrfval2  7194  fmpt2x  7518  ovmptss  7541  cbvixp  8213  mptelixpg  8233  boxcutc  8239  xpf1o  8412  indexfi  8564  ixpiunwdom  8787  dfac8clem  9190  acni2  9204  ac6c4  9640  iundom2g  9699  uniimadomf  9704  rabssnn0fi  13109  rlim2  14644  ello1mpt  14669  o1compt  14735  fsum00  14943  iserodd  15955  pcmptdvds  16013  catpropd  16765  invfuc  17030  gsummptnn0fz  18779  gsummptnn0fzOLD  18780  gsummoncoe1  20081  gsumply1eq  20082  fiuncmp  21627  elptr2  21797  ptcld  21836  ptclsg  21838  ptcnplem  21844  cnmpt11  21886  cnmpt21  21894  ovoliunlem3  23719  ovoliun  23720  ovoliun2  23721  finiunmbl  23759  volfiniun  23762  iunmbl  23768  voliun  23769  mbfeqalem1  23856  mbfsup  23879  mbfinf  23880  mbflim  23883  itg2split  23964  itgeqa  24028  itgfsum  24041  itgabs  24049  itggt0  24056  limciun  24106  dvlipcn  24205  dvfsumlem4  24240  dvfsum2  24245  itgsubst  24260  coeeq2  24446  ulmss  24599  leibpi  25132  rlimcnp  25155  o1cxp  25164  lgamgulmlem6  25223  fsumdvdscom  25374  lgseisenlem2  25564  disjunsn  29987  bnj110  31535  bnj1529  31745  poimirlem23  34067  itgabsnc  34113  itggt0cn  34116  totbndbnd  34221  disjinfi  40317  fmptf  40376  climinff  40765  idlimc  40780  fnlimabslt  40833  limsupref  40839  limsupbnd1f  40840  climbddf  40841  climinf2  40861  limsupubuz  40867  climinfmpt  40869  limsupmnf  40875  limsupre2  40879  limsupmnfuz  40881  limsupre3  40887  limsupre3uz  40890  limsupreuz  40891  climuz  40898  lmbr3  40901  liminflelimsup  40930  limsupgt  40932  liminfreuz  40957  liminflt  40959  xlimpnfxnegmnf  40968  xlimmnf  40995  xlimpnf  40996  dfxlim2  41002  cncfshift  41029  stoweidlem31  41189  iundjiun  41615  meaiunincf  41638  pimgtmnf2  41865  smfpimcc  41955  smfsup  41961  smfinflem  41964  smfinf  41965  cbvral2  42145