Theorem cbvral 3155

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

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1705  ∀wral 2907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912

This theorem is referenced by:  cbvralv  3159  cbvralsv  3170  cbviin  4524  disjxun  4611  ralxpf  5228  eqfnfv2f  6271  ralrnmpt  6324  dff13f  6467  ofrfval2  6868  fmpt2x  7181  ovmptss  7203  cbvixp  7869  mptelixpg  7889  boxcutc  7895  xpf1o  8066  indexfi  8218  ixpiunwdom  8440  dfac8clem  8799  acni2  8813  ac6num  9245  ac6c4  9247  iundom2g  9306  uniimadomf  9311  rabssnn0fi  12725  rlim2  14161  ello1mpt  14186  o1compt  14252  fsum00  14457  iserodd  15464  pcmptdvds  15522  catpropd  16290  invfuc  16555  gsummptnn0fz  18303  gsummoncoe1  19593  gsumply1eq  19594  fiuncmp  21117  elptr2  21287  ptcld  21326  ptclsg  21328  ptcnplem  21334  cnmpt11  21376  cnmpt21  21384  ovoliunlem3  23179  ovoliun  23180  ovoliun2  23181  finiunmbl  23219  volfiniun  23222  iunmbl  23228  voliun  23229  mbfeqalem  23315  mbfsup  23337  mbfinf  23338  mbflim  23341  itg2split  23422  itgeqa  23486  itgfsum  23499  itgabs  23507  itggt0  23514  limciun  23564  dvlipcn  23661  dvfsumlem4  23696  dvfsum2  23701  itgsubst  23716  coeeq2  23902  ulmss  24055  leibpi  24569  rlimcnp  24592  o1cxp  24601  lgamgulmlem6  24660  fsumdvdscom  24811  lgseisenlem2  25001  disjunsn  29252  bnj110  30636  bnj1529  30846  poimirlem23  33064  itgabsnc  33111  itggt0cn  33114  totbndbnd  33220  disjinfi  38854  fmptf  38923  climinff  39247  idlimc  39262  fnlimabslt  39315  limsupref  39321  limsupbnd1f  39322  climbddf  39323  climinf2  39343  limsupubuz  39349  climinfmpt  39351  limsupmnf  39357  limsupre2  39361  limsupmnfuz  39363  limsupre3  39369  limsupre3uz  39372  limsupreuz  39373  cncfshift  39390  stoweidlem31  39555  iundjiun  39984  pimgtmnf2  40231  smfpimcc  40321  smfsup  40327  smfinflem  40330  smfinf  40331  cbvral2  40476