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  2931  rspc2  2934  rspc3v  2939  reu6i  3010  reu7  3014  sbcralt  3121  sbcralg  3123  reu8nf  3126  raaanlem  3616  2ralunsn  3905  elintg  3959  elintrabg  3964  eliin  3998  brralrspcev  4170  bnd2  4288  poeq1  4422  soeq1  4438  frforeq1  4466  frforeq3  4470  frirrg  4473  frind  4475  weeq1  4479  reusv3  4583  ontr2exmid  4649  reg2exmidlema  4658  posng  4824  ralxpf  4903  cnvpom  5307  funcnvuni  5427  fnmptfvd  5784  dff4im  5825  dff13f  5945  eusvobj2  6038  ovanraleqv  6076  ofreq  6272  caofdig  6302  uchoice  6333  suppssrst  6463  suppssrgst  6464  suppofss1dcl  6466  suppofss2dcl  6467  smoeq  6523  recseq  6539  tfr0dm  6555  tfrlemiex  6564  tfr1onlemex  6580  tfr1onlemaccex  6581  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllemex  6593  tfrcllemaccex  6594  tfrcllemres  6595  elixp2  6939  pw2f1odclem  7089  xpf1o  7099  nneneq  7113  ac6sfi  7157  fimax2gtrilemstep  7160  fimax2gtri  7161  elssdc  7164  opabfi  7202  2omap  7271  supeq1  7279  supeq3  7283  supmoti  7286  eqsupti  7289  supubti  7292  suplubti  7293  supisoex  7302  cnvinfex  7311  eqinfti  7313  infvalti  7315  updjud  7375  ctssdclemr  7405  nninff  7415  nninfninc  7416  infnninf  7417  infnninfOLD  7418  nnnninf  7419  nnnninfeq  7421  nnnninfeq2  7422  enomnilem  7431  finomni  7433  exmidomni  7435  fodjuomnilemres  7441  ismkvnex  7448  fodjumkvlemres  7452  enmkvlem  7454  enwomnilem  7462  nninfdcinf  7464  nninfwlporlem  7466  nninfwlpoimlemg  7468  nninfwlpoimlemdc  7470  exmidontriimlem3  7532  exmidontriim  7534  papsym  7563  papcotr  7564  tapeq1  7568  netap  7570  exmidapne  7576  cc2lem  7582  cc3  7584  elinp  7791  prloc  7808  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  caucvgpr  7999  caucvgprpr  8029  suplocexprlemloc  8038  suplocexpr  8042  caucvgsrlemgt1  8112  caucvgsrlemoffres  8117  caucvgsr  8119  suplocsrlemb  8123  suplocsrlempr  8124  suplocsrlem  8125  axcaucvglemcau  8215  axcaucvglemres  8216  axpre-suploclemres  8218  axpre-suploc  8219  lbreu  9221  sup3exmid  9233  nnsub  9278  indstr  9928  supinfneg  9930  infsupneg  9931  ublbneg  9948  lbzbi  9951  iccsupr  10302  zsupcllemstep  10593  infssuzex  10597  suprzubdc  10600  nninfdcex  10601  zsupssdc  10602  frecuzrdgsuc  10780  frecuzrdgg  10782  frecuzrdgsuctlem  10789  seq3f1olemstep  10880  seq3f1olemp  10881  seqfeq4g  10897  nn0ltexp2  11075  bccl  11133  hashfibc  11211  wrdind  11418  wrd2ind  11419  cau4  11805  caubnd2  11806  maxleast  11902  rexanre  11909  rexico  11910  fimaxre2  11916  minmax  11919  xrminmax  11954  clim  11970  clim2  11972  clim2c  11973  clim0c  11975  climabs0  11996  cn1lem  12003  sumeq1  12044  prodeq1f  12242  bezoutlemstep  12697  bezoutlemmain  12698  bezoutlemex  12701  bezoutlemeu  12707  dfgcd3  12710  bezout  12711  dfgcd2  12714  nnwodc  12736  uzwodc  12737  nnwofdc  12738  sqrt2irr  12863  reumodprminv  12955  pc2dvds  13032  pcz  13034  prmpwdvds  13057  ballotfileme  13157  ennnfoneleminc  13179  ennnfonelemex  13182  ennnfonelemhom  13183  ennnfonelemnn0  13190  ennnfonelemr  13191  ennnfonelemim  13192  exmidunben  13194  ctinfomlemom  13195  ctinfom  13196  ctinf  13198  ctiunctlemudc  13205  ctiunct  13208  ssomct  13213  infpn2  13224  imasaddfnlemg  13544  mgm1  13600  sgrp1  13641  mhmima  13721  dfgrp2  13757  isgrpinv  13784  grpidinv  13789  dfgrp3mlem  13828  issubg4m  13927  isnsg2  13937  elnmz  13942  ghmrn  13991  ghmnsgima  14002  srgideu  14133  ring1  14220  lringuplu  14358  subrgugrp  14402  isrrg  14425  islssm  14522  islssmg  14523  rnglidlmcl  14645  mplsubgfilemm  14870  mplsubgfilemcl  14871  basgen2  14963  bastop1  14965  iscn  15079  cnpval  15080  iscnp  15081  iscnp3  15085  cnprcl2k  15088  lmbr  15095  lmbr2  15096  lmbrf  15097  cnptoprest  15121  cnptoprest2  15122  cnmpt21  15173  ispsmet  15205  ismet  15226  isxmet  15227  metss  15376  qtopbasss  15403  cncfval  15454  elcncf2  15456  mulc1cncf  15471  cncfmet  15474  dedekindeulemloc  15501  dedekindeulemeu  15504  dedekindeu  15505  suplociccreex  15506  dedekindicclemloc  15510  dedekindicclemeu  15513  dedekindicclemicc  15514  ivthinclemlopn  15518  ivthinclemlr  15519  ivthinclemuopn  15520  ivthinclemur  15521  ivthinclemloc  15523  ivthreinc  15527  dich0  15534  limccl  15541  ellimc3apf  15542  limcdifap  15544  limcmpted  15545  2irrexpqap  15860  perfectlem2  15885  2sqlem6  16010  2sqlem10  16015  wksfval  16334  wlkvtxedg  16375  clwwlkg  16405  depind  16521  bj-charfunbi  16598  bj-omtrans  16743  strcoll2  16770  strcollnfALT  16773  sscoll2  16775  pw1nct  16794  exmidcon  16797  0nninf  16799  nnsf  16800  peano4nninf  16801  nninfalllem1  16803  nninfself  16808  nninfsellemeq  16809  nninfsellemeqinf  16811  isomninnlem  16831  trilpolemlt1  16842  iswomninnlem  16851  iswomni0  16853  ismkvnnlem  16854  cndcap  16861  dceqnconst  16863  dcapnconst  16864  ltlenmkv  16873