Theorem cbvral 3167

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

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1708  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917

This theorem is referenced by:  cbvralv  3171  cbvralsv  3182  cbviin  4558  disjxun  4651  ralxpf  5268  eqfnfv2f  6315  ralrnmpt  6368  dff13f  6513  ofrfval2  6915  fmpt2x  7236  ovmptss  7258  cbvixp  7925  mptelixpg  7945  boxcutc  7951  xpf1o  8122  indexfi  8274  ixpiunwdom  8496  dfac8clem  8855  acni2  8869  ac6num  9301  ac6c4  9303  iundom2g  9362  uniimadomf  9367  rabssnn0fi  12785  rlim2  14227  ello1mpt  14252  o1compt  14318  fsum00  14530  iserodd  15540  pcmptdvds  15598  catpropd  16369  invfuc  16634  gsummptnn0fz  18382  gsummoncoe1  19674  gsumply1eq  19675  fiuncmp  21207  elptr2  21377  ptcld  21416  ptclsg  21418  ptcnplem  21424  cnmpt11  21466  cnmpt21  21474  ovoliunlem3  23272  ovoliun  23273  ovoliun2  23274  finiunmbl  23312  volfiniun  23315  iunmbl  23321  voliun  23322  mbfeqalem  23409  mbfsup  23431  mbfinf  23432  mbflim  23435  itg2split  23516  itgeqa  23580  itgfsum  23593  itgabs  23601  itggt0  23608  limciun  23658  dvlipcn  23757  dvfsumlem4  23792  dvfsum2  23797  itgsubst  23812  coeeq2  23998  ulmss  24151  leibpi  24669  rlimcnp  24692  o1cxp  24701  lgamgulmlem6  24760  fsumdvdscom  24911  lgseisenlem2  25101  disjunsn  29407  bnj110  30928  bnj1529  31138  poimirlem23  33432  itgabsnc  33479  itggt0cn  33482  totbndbnd  33588  disjinfi  39380  fmptf  39448  climinff  39843  idlimc  39858  fnlimabslt  39911  limsupref  39917  limsupbnd1f  39918  climbddf  39919  climinf2  39939  limsupubuz  39945  climinfmpt  39947  limsupmnf  39953  limsupre2  39957  limsupmnfuz  39959  limsupre3  39965  limsupre3uz  39968  limsupreuz  39969  climuz  39976  lmbr3  39979  liminflelimsup  40008  limsupgt  40010  liminfreuz  40035  liminflt  40037  xlimmnf  40067  xlimpnf  40068  dfxlim2  40074  cncfshift  40087  stoweidlem31  40248  iundjiun  40677  pimgtmnf2  40924  smfpimcc  41014  smfsup  41020  smfinflem  41023  smfinf  41024  cbvral2  41172