Theorem ralbidv 2544

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ralbidv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		nfv 1577	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	ralbid 2542	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  ralbii  2550  2ralbidv  2568  rexralbidv  2570  r19.32vdc  2694  raleqbi1dv  2755  raleqbidv  2759  cbvral2vw  2791  cbvral2v  2793  rspceaimv  2932  rspc2  2935  rspc3v  2940  reu6i  3011  reu7  3015  sbcralt  3122  sbcralg  3124  reu8nf  3127  raaanlem  3618  2ralunsn  3908  elintg  3962  elintrabg  3967  eliin  4001  brralrspcev  4173  bnd2  4291  poeq1  4425  soeq1  4441  frforeq1  4469  frforeq3  4473  frirrg  4476  frind  4478  weeq1  4482  reusv3  4586  ontr2exmid  4652  reg2exmidlema  4661  posng  4827  ralxpf  4906  cnvpom  5310  funcnvuni  5430  fnmptfvd  5787  dff4im  5828  dff13f  5949  eusvobj2  6044  ovanraleqv  6082  ofreq  6279  caofdig  6309  uchoice  6344  suppssrst  6474  suppssrgst  6475  suppofss1dcl  6477  suppofss2dcl  6478  smoeq  6534  recseq  6550  tfr0dm  6566  tfrlemiex  6575  tfr1onlemex  6591  tfr1onlemaccex  6592  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemex  6604  tfrcllemaccex  6605  tfrcllemres  6606  elixp2  6950  pw2f1odclem  7100  xpf1o  7110  nneneq  7124  ac6sfi  7168  fimax2gtrilemstep  7171  fimax2gtri  7172  elssdc  7175  opabfi  7213  2omap  7282  supeq1  7290  supeq3  7294  supmoti  7297  eqsupti  7300  supubti  7303  suplubti  7304  supisoex  7313  cnvinfex  7322  eqinfti  7324  infvalti  7326  updjud  7386  ctssdclemr  7416  nninff  7426  nninfninc  7427  infnninf  7428  infnninfOLD  7429  nnnninf  7430  nnnninfeq  7432  nnnninfeq2  7433  enomnilem  7442  finomni  7444  exmidomni  7446  fodjuomnilemres  7452  ismkvnex  7459  fodjumkvlemres  7463  enmkvlem  7465  enwomnilem  7473  nninfdcinf  7475  nninfwlporlem  7477  nninfwlpoimlemg  7479  nninfwlpoimlemdc  7481  exmidontriimlem3  7543  exmidontriim  7545  papeq1  7573  papsym  7576  papcotr  7577  tapeq1  7582  netap  7584  exmidapne  7590  cc2lem  7596  cc3  7598  elinp  7805  prloc  7822  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgpr  8013  caucvgprpr  8043  suplocexprlemloc  8052  suplocexpr  8056  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  lbreu  9239  sup3exmid  9251  nnsub  9296  indstr  9946  supinfneg  9948  infsupneg  9949  ublbneg  9966  lbzbi  9969  iccsupr  10321  zsupcllemstep  10614  infssuzex  10618  suprzubdc  10623  nninfdcex  10624  zsupssdc  10625  frecuzrdgsuc  10803  frecuzrdgg  10805  frecuzrdgsuctlem  10812  seq3f1olemstep  10903  seq3f1olemp  10904  seqfeq4g  10920  nn0ltexp2  11099  bccl  11157  hashfibc  11235  wrdind  11442  wrd2ind  11443  cau4  11829  caubnd2  11830  maxleast  11926  rexanre  11933  rexico  11934  fimaxre2  11940  minmax  11943  xrminmax  11978  clim  11994  clim2  11996  clim2c  11997  clim0c  11999  climabs0  12020  cn1lem  12027  sumeq1  12068  prodeq1f  12266  bezoutlemstep  12721  bezoutlemmain  12722  bezoutlemex  12725  bezoutlemeu  12731  dfgcd3  12734  bezout  12735  dfgcd2  12738  nnwodc  12760  uzwodc  12761  nnwofdc  12762  sqrt2irr  12887  reumodprminv  12979  pc2dvds  13056  pcz  13058  prmpwdvds  13081  ballotfileme  13183  ennnfoneleminc  13249  ennnfonelemex  13252  ennnfonelemhom  13253  ennnfonelemnn0  13260  ennnfonelemr  13261  ennnfonelemim  13262  exmidunben  13264  ctinfomlemom  13265  ctinfom  13266  ctinf  13268  ctiunctlemudc  13275  ctiunct  13278  ssomct  13283  infpn2  13294  imasaddfnlemg  13581  mgm1  13636  sgrp1  13677  mhmima  13749  dfgrp2  13785  isgrpinv  13812  grpidinv  13817  dfgrp3mlem  13856  issubg4m  13949  isnsg2  13959  elnmz  13964  ghmrn  14013  ghmnsgima  14024  srgideu  14218  ring1  14305  lringuplu  14444  subrgugrp  14489  isrrg  14512  islssm  14634  islssmg  14635  rnglidlmcl  14757  mplsubgfilemm  14982  mplsubgfilemcl  14983  basgen2  15075  bastop1  15077  iscn  15191  cnpval  15192  iscnp  15193  iscnp3  15197  cnprcl2k  15200  lmbr  15207  lmbr2  15208  lmbrf  15209  cnptoprest  15233  cnptoprest2  15234  cnmpt21  15285  ispsmet  15317  ismet  15338  isxmet  15339  metss  15488  qtopbasss  15515  cncfval  15566  elcncf2  15568  mulc1cncf  15583  cncfmet  15586  dedekindeulemloc  15613  dedekindeulemeu  15616  dedekindeu  15617  suplociccreex  15618  dedekindicclemloc  15622  dedekindicclemeu  15625  dedekindicclemicc  15626  ivthinclemlopn  15630  ivthinclemlr  15631  ivthinclemuopn  15632  ivthinclemur  15633  ivthinclemloc  15635  ivthreinc  15639  dich0  15646  limccl  15653  ellimc3apf  15654  limcdifap  15656  limcmpted  15657  2irrexpqap  15972  perfectlem2  15997  2sqlem6  16122  2sqlem10  16127  wksfval  16446  wlkvtxedg  16487  clwwlkg  16517  depind  16633  bj-charfunbi  16720  bj-omtrans  16865  strcoll2  16892  strcollnfALT  16895  sscoll2  16897  pw1nct  16916  exmidcon  16919  0nninf  16921  nnsf  16922  peano4nninf  16923  nninfalllem1  16925  nninfself  16930  nninfsellemeq  16931  nninfsellemeqinf  16933  isomninnlem  16953  trilpolemlt1  16964  iswomninnlem  16973  iswomni0  16975  ismkvnnlem  16976  cndcap  16983  dceqnconst  16985  dcapnconst  16986  ltlenmkv  16995