Theorem ralbidv 2532

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 1576	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	ralbid 2530	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralbii  2538  2ralbidv  2556  rexralbidv  2558  r19.32vdc  2682  raleqbi1dv  2742  raleqbidv  2746  cbvral2vw  2778  cbvral2v  2780  rspceaimv  2918  rspc2  2921  rspc3v  2926  reu6i  2997  reu7  3001  sbcralt  3108  sbcralg  3110  reu8nf  3113  raaanlem  3599  2ralunsn  3882  elintg  3936  elintrabg  3941  eliin  3975  brralrspcev  4147  bnd2  4263  poeq1  4396  soeq1  4412  frforeq1  4440  frforeq3  4444  frirrg  4447  frind  4449  weeq1  4453  reusv3  4557  ontr2exmid  4623  reg2exmidlema  4632  posng  4798  ralxpf  4876  cnvpom  5279  funcnvuni  5399  fnmptfvd  5751  dff4im  5793  dff13f  5910  eusvobj2  6003  ovanraleqv  6041  ofreq  6238  caofdig  6268  uchoice  6299  smoeq  6455  recseq  6471  tfr0dm  6487  tfrlemiex  6496  tfr1onlemex  6512  tfr1onlemaccex  6513  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemex  6525  tfrcllemaccex  6526  tfrcllemres  6527  elixp2  6870  pw2f1odclem  7019  xpf1o  7029  nneneq  7042  ac6sfi  7086  fimax2gtrilemstep  7089  fimax2gtri  7090  elssdc  7093  opabfi  7131  supeq1  7184  supeq3  7188  supmoti  7191  eqsupti  7194  supubti  7197  suplubti  7198  supisoex  7207  cnvinfex  7216  eqinfti  7218  infvalti  7220  updjud  7280  ctssdclemr  7310  nninff  7320  nninfninc  7321  infnninf  7322  infnninfOLD  7323  nnnninf  7324  nnnninfeq  7326  nnnninfeq2  7327  enomnilem  7336  finomni  7338  exmidomni  7340  fodjuomnilemres  7346  ismkvnex  7353  fodjumkvlemres  7357  enmkvlem  7359  enwomnilem  7367  nninfdcinf  7369  nninfwlporlem  7371  nninfwlpoimlemg  7373  nninfwlpoimlemdc  7375  exmidontriimlem3  7437  exmidontriim  7439  tapeq1  7470  netap  7472  exmidapne  7478  cc2lem  7484  cc3  7486  elinp  7693  prloc  7710  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgpr  7901  caucvgprpr  7931  suplocexprlemloc  7940  suplocexpr  7944  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  caucvgsr  8021  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axcaucvglemcau  8117  axcaucvglemres  8118  axpre-suploclemres  8120  axpre-suploc  8121  lbreu  9124  sup3exmid  9136  nnsub  9181  indstr  9826  supinfneg  9828  infsupneg  9829  ublbneg  9846  lbzbi  9849  iccsupr  10200  zsupcllemstep  10488  infssuzex  10492  suprzubdc  10495  nninfdcex  10496  zsupssdc  10497  frecuzrdgsuc  10675  frecuzrdgg  10677  frecuzrdgsuctlem  10684  seq3f1olemstep  10775  seq3f1olemp  10776  seqfeq4g  10792  nn0ltexp2  10970  bccl  11028  wrdind  11302  wrd2ind  11303  cau4  11676  caubnd2  11677  maxleast  11773  rexanre  11780  rexico  11781  fimaxre2  11787  minmax  11790  xrminmax  11825  clim  11841  clim2  11843  clim2c  11844  clim0c  11846  climabs0  11867  cn1lem  11874  sumeq1  11915  prodeq1f  12112  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlemex  12571  bezoutlemeu  12577  dfgcd3  12580  bezout  12581  dfgcd2  12584  nnwodc  12606  uzwodc  12607  nnwofdc  12608  sqrt2irr  12733  reumodprminv  12825  pc2dvds  12902  pcz  12904  prmpwdvds  12927  ennnfoneleminc  13031  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemnn0  13042  ennnfonelemr  13043  ennnfonelemim  13044  exmidunben  13046  ctinfomlemom  13047  ctinfom  13048  ctinf  13050  ctiunctlemudc  13057  ctiunct  13060  ssomct  13065  infpn2  13076  imasaddfnlemg  13396  mgm1  13452  sgrp1  13493  mhmima  13573  dfgrp2  13609  isgrpinv  13636  grpidinv  13641  dfgrp3mlem  13680  issubg4m  13779  isnsg2  13789  elnmz  13794  ghmrn  13843  ghmnsgima  13854  srgideu  13984  ring1  14071  lringuplu  14209  subrgugrp  14253  isrrg  14276  islssm  14370  islssmg  14371  rnglidlmcl  14493  mplsubgfilemm  14711  mplsubgfilemcl  14712  basgen2  14804  bastop1  14806  iscn  14920  cnpval  14921  iscnp  14922  iscnp3  14926  cnprcl2k  14929  lmbr  14936  lmbr2  14937  lmbrf  14938  cnptoprest  14962  cnptoprest2  14963  cnmpt21  15014  ispsmet  15046  ismet  15067  isxmet  15068  metss  15217  qtopbasss  15244  cncfval  15295  elcncf2  15297  mulc1cncf  15312  cncfmet  15315  dedekindeulemloc  15342  dedekindeulemeu  15345  dedekindeu  15346  suplociccreex  15347  dedekindicclemloc  15351  dedekindicclemeu  15354  dedekindicclemicc  15355  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemloc  15364  ivthreinc  15368  dich0  15375  limccl  15382  ellimc3apf  15383  limcdifap  15385  limcmpted  15386  2irrexpqap  15701  perfectlem2  15723  2sqlem6  15848  2sqlem10  15853  wksfval  16172  wlkvtxedg  16213  clwwlkg  16243  bj-charfunbi  16406  bj-omtrans  16551  strcoll2  16578  strcollnfALT  16581  sscoll2  16583  2omap  16594  pw1nct  16604  0nninf  16606  nnsf  16607  peano4nninf  16608  nninfalllem1  16610  nninfself  16615  nninfsellemeq  16616  nninfsellemeqinf  16618  isomninnlem  16634  trilpolemlt1  16645  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656  cndcap  16663  dceqnconst  16664  dcapnconst  16665  ltlenmkv  16674