Theorem cbvral 3143

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

Syntax hints:   → wi 4   ↔ wb 195  Ⅎwnf 1699  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901

This theorem is referenced by:  cbvralv  3147  cbvralsv  3158  cbviin  4494  disjxun  4581  ralxpf  5190  eqfnfv2f  6223  ralrnmpt  6276  dff13f  6417  ofrfval2  6813  fmpt2x  7125  ovmptss  7145  cbvixp  7811  mptelixpg  7831  boxcutc  7837  xpf1o  8007  indexfi  8157  ixpiunwdom  8379  dfac8clem  8738  acni2  8752  ac6num  9184  ac6c4  9186  iundom2g  9241  uniimadomf  9246  rabssnn0fi  12647  rlim2  14075  ello1mpt  14100  o1compt  14166  fsum00  14371  iserodd  15378  pcmptdvds  15436  catpropd  16192  invfuc  16457  gsummptnn0fz  18205  gsummoncoe1  19495  gsumply1eq  19496  fiuncmp  21017  elptr2  21187  ptcld  21226  ptclsg  21228  ptcnplem  21234  cnmpt11  21276  cnmpt21  21284  ovoliunlem3  23079  ovoliun  23080  ovoliun2  23081  finiunmbl  23119  volfiniun  23122  iunmbl  23128  voliun  23129  mbfeqalem  23215  mbfsup  23237  mbfinf  23238  mbflim  23241  itg2split  23322  itgeqa  23386  itgfsum  23399  itgabs  23407  itggt0  23414  limciun  23464  dvlipcn  23561  dvfsumlem4  23596  dvfsum2  23601  itgsubst  23616  coeeq2  23802  ulmss  23955  leibpi  24469  rlimcnp  24492  o1cxp  24501  lgamgulmlem6  24560  fsumdvdscom  24711  lgseisenlem2  24901  disjunsn  28789  bnj110  30182  bnj1529  30392  poimirlem23  32602  itgabsnc  32649  itggt0cn  32652  totbndbnd  32758  disjinfi  38375  climinff  38678  idlimc  38693  fnlimabslt  38746  cncfshift  38759  stoweidlem31  38924  iundjiun  39353  pimgtmnf2  39601  cbvral2  39821