Theorem ralbidv 2508

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

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  ralbii  2514  2ralbidv  2532  rexralbidv  2534  r19.32vdc  2657  raleqbi1dv  2717  raleqbidv  2721  cbvral2vw  2753  cbvral2v  2755  rspceaimv  2892  rspc2  2895  rspc3v  2900  reu6i  2971  reu7  2975  sbcralt  3082  sbcralg  3084  reu8nf  3087  raaanlem  3573  2ralunsn  3853  elintg  3907  elintrabg  3912  eliin  3946  brralrspcev  4118  bnd2  4233  poeq1  4364  soeq1  4380  frforeq1  4408  frforeq3  4412  frirrg  4415  frind  4417  weeq1  4421  reusv3  4525  ontr2exmid  4591  reg2exmidlema  4600  posng  4765  ralxpf  4842  cnvpom  5244  funcnvuni  5362  fnmptfvd  5707  dff4im  5749  dff13f  5862  eusvobj2  5953  ovanraleqv  5991  ofreq  6185  caofdig  6215  uchoice  6246  smoeq  6399  recseq  6415  tfr0dm  6431  tfrlemiex  6440  tfr1onlemex  6456  tfr1onlemaccex  6457  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllemex  6469  tfrcllemaccex  6470  tfrcllemres  6471  elixp2  6812  pw2f1odclem  6956  xpf1o  6966  nneneq  6979  ac6sfi  7021  fimax2gtrilemstep  7023  fimax2gtri  7024  opabfi  7061  supeq1  7114  supeq3  7118  supmoti  7121  eqsupti  7124  supubti  7127  suplubti  7128  supisoex  7137  cnvinfex  7146  eqinfti  7148  infvalti  7150  updjud  7210  ctssdclemr  7240  nninff  7250  nninfninc  7251  infnninf  7252  infnninfOLD  7253  nnnninf  7254  nnnninfeq  7256  nnnninfeq2  7257  enomnilem  7266  finomni  7268  exmidomni  7270  fodjuomnilemres  7276  ismkvnex  7283  fodjumkvlemres  7287  enmkvlem  7289  enwomnilem  7297  nninfdcinf  7299  nninfwlporlem  7301  nninfwlpoimlemg  7303  nninfwlpoimlemdc  7305  exmidontriimlem3  7366  exmidontriim  7368  tapeq1  7399  netap  7401  exmidapne  7407  cc2lem  7413  cc3  7415  elinp  7622  prloc  7639  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgpr  7830  caucvgprpr  7860  suplocexprlemloc  7869  suplocexpr  7873  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  caucvgsr  7950  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  axcaucvglemcau  8046  axcaucvglemres  8047  axpre-suploclemres  8049  axpre-suploc  8050  lbreu  9053  sup3exmid  9065  nnsub  9110  indstr  9749  supinfneg  9751  infsupneg  9752  ublbneg  9769  lbzbi  9772  iccsupr  10123  zsupcllemstep  10409  infssuzex  10413  suprzubdc  10416  nninfdcex  10417  zsupssdc  10418  frecuzrdgsuc  10596  frecuzrdgg  10598  frecuzrdgsuctlem  10605  seq3f1olemstep  10696  seq3f1olemp  10697  seqfeq4g  10713  nn0ltexp2  10891  bccl  10949  wrdind  11213  wrd2ind  11214  cau4  11542  caubnd2  11543  maxleast  11639  rexanre  11646  rexico  11647  fimaxre2  11653  minmax  11656  xrminmax  11691  clim  11707  clim2  11709  clim2c  11710  clim0c  11712  climabs0  11733  cn1lem  11740  sumeq1  11781  prodeq1f  11978  bezoutlemstep  12433  bezoutlemmain  12434  bezoutlemex  12437  bezoutlemeu  12443  dfgcd3  12446  bezout  12447  dfgcd2  12450  nnwodc  12472  uzwodc  12473  nnwofdc  12474  sqrt2irr  12599  reumodprminv  12691  pc2dvds  12768  pcz  12770  prmpwdvds  12793  ennnfoneleminc  12897  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemnn0  12908  ennnfonelemr  12909  ennnfonelemim  12910  exmidunben  12912  ctinfomlemom  12913  ctinfom  12914  ctinf  12916  ctiunctlemudc  12923  ctiunct  12926  ssomct  12931  infpn2  12942  imasaddfnlemg  13261  mgm1  13317  sgrp1  13358  mhmima  13438  dfgrp2  13474  isgrpinv  13501  grpidinv  13506  dfgrp3mlem  13545  issubg4m  13644  isnsg2  13654  elnmz  13659  ghmrn  13708  ghmnsgima  13719  srgideu  13849  ring1  13936  lringuplu  14073  subrgugrp  14117  isrrg  14140  islssm  14234  islssmg  14235  rnglidlmcl  14357  mplsubgfilemm  14575  mplsubgfilemcl  14576  basgen2  14668  bastop1  14670  iscn  14784  cnpval  14785  iscnp  14786  iscnp3  14790  cnprcl2k  14793  lmbr  14800  lmbr2  14801  lmbrf  14802  cnptoprest  14826  cnptoprest2  14827  cnmpt21  14878  ispsmet  14910  ismet  14931  isxmet  14932  metss  15081  qtopbasss  15108  cncfval  15159  elcncf2  15161  mulc1cncf  15176  cncfmet  15179  dedekindeulemloc  15206  dedekindeulemeu  15209  dedekindeu  15210  suplociccreex  15211  dedekindicclemloc  15215  dedekindicclemeu  15218  dedekindicclemicc  15219  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemloc  15228  ivthreinc  15232  dich0  15239  limccl  15246  ellimc3apf  15247  limcdifap  15249  limcmpted  15250  2irrexpqap  15565  perfectlem2  15587  2sqlem6  15712  2sqlem10  15717  bj-charfunbi  15946  bj-omtrans  16091  strcoll2  16118  strcollnfALT  16121  sscoll2  16123  2omap  16132  pw1nct  16142  0nninf  16143  nnsf  16144  peano4nninf  16145  nninfalllem1  16147  nninfself  16152  nninfsellemeq  16153  nninfsellemeqinf  16155  isomninnlem  16171  trilpolemlt1  16182  iswomninnlem  16190  iswomni0  16192  ismkvnnlem  16193  cndcap  16200  dceqnconst  16201  dcapnconst  16202  ltlenmkv  16211