Theorem ralbidv 2506

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  ralbii  2512  2ralbidv  2530  rexralbidv  2532  r19.32vdc  2655  raleqbi1dv  2714  raleqbidv  2718  cbvral2vw  2749  cbvral2v  2751  rspceaimv  2885  rspc2  2888  rspc3v  2893  reu6i  2964  reu7  2968  sbcralt  3075  sbcralg  3077  raaanlem  3565  2ralunsn  3839  elintg  3893  elintrabg  3898  eliin  3932  brralrspcev  4103  bnd2  4218  poeq1  4347  soeq1  4363  frforeq1  4391  frforeq3  4395  frirrg  4398  frind  4400  weeq1  4404  reusv3  4508  ontr2exmid  4574  reg2exmidlema  4583  posng  4748  ralxpf  4825  cnvpom  5226  funcnvuni  5344  fnmptfvd  5686  dff4im  5728  dff13f  5841  eusvobj2  5932  ovanraleqv  5970  ofreq  6164  caofdig  6194  uchoice  6225  smoeq  6378  recseq  6394  tfr0dm  6410  tfrlemiex  6419  tfr1onlemex  6435  tfr1onlemaccex  6436  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllemex  6448  tfrcllemaccex  6449  tfrcllemres  6450  elixp2  6791  pw2f1odclem  6933  xpf1o  6943  nneneq  6956  ac6sfi  6997  fimax2gtrilemstep  6999  fimax2gtri  7000  opabfi  7037  supeq1  7090  supeq3  7094  supmoti  7097  eqsupti  7100  supubti  7103  suplubti  7104  supisoex  7113  cnvinfex  7122  eqinfti  7124  infvalti  7126  updjud  7186  ctssdclemr  7216  nninff  7226  nninfninc  7227  infnninf  7228  infnninfOLD  7229  nnnninf  7230  nnnninfeq  7232  nnnninfeq2  7233  enomnilem  7242  finomni  7244  exmidomni  7246  fodjuomnilemres  7252  ismkvnex  7259  fodjumkvlemres  7263  enmkvlem  7265  enwomnilem  7273  nninfdcinf  7275  nninfwlporlem  7277  nninfwlpoimlemg  7279  nninfwlpoimlemdc  7281  exmidontriimlem3  7337  exmidontriim  7339  tapeq1  7366  netap  7368  exmidapne  7374  cc2lem  7380  cc3  7382  elinp  7589  prloc  7606  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  caucvgpr  7797  caucvgprpr  7827  suplocexprlemloc  7836  suplocexpr  7840  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  caucvgsr  7917  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  axcaucvglemcau  8013  axcaucvglemres  8014  axpre-suploclemres  8016  axpre-suploc  8017  lbreu  9020  sup3exmid  9032  nnsub  9077  indstr  9716  supinfneg  9718  infsupneg  9719  ublbneg  9736  lbzbi  9739  iccsupr  10090  zsupcllemstep  10374  infssuzex  10378  suprzubdc  10381  nninfdcex  10382  zsupssdc  10383  frecuzrdgsuc  10561  frecuzrdgg  10563  frecuzrdgsuctlem  10570  seq3f1olemstep  10661  seq3f1olemp  10662  seqfeq4g  10678  nn0ltexp2  10856  bccl  10914  cau4  11460  caubnd2  11461  maxleast  11557  rexanre  11564  rexico  11565  fimaxre2  11571  minmax  11574  xrminmax  11609  clim  11625  clim2  11627  clim2c  11628  clim0c  11630  climabs0  11651  cn1lem  11658  sumeq1  11699  prodeq1f  11896  bezoutlemstep  12351  bezoutlemmain  12352  bezoutlemex  12355  bezoutlemeu  12361  dfgcd3  12364  bezout  12365  dfgcd2  12368  nnwodc  12390  uzwodc  12391  nnwofdc  12392  sqrt2irr  12517  reumodprminv  12609  pc2dvds  12686  pcz  12688  prmpwdvds  12711  ennnfoneleminc  12815  ennnfonelemex  12818  ennnfonelemhom  12819  ennnfonelemnn0  12826  ennnfonelemr  12827  ennnfonelemim  12828  exmidunben  12830  ctinfomlemom  12831  ctinfom  12832  ctinf  12834  ctiunctlemudc  12841  ctiunct  12844  ssomct  12849  infpn2  12860  imasaddfnlemg  13179  mgm1  13235  sgrp1  13276  mhmima  13356  dfgrp2  13392  isgrpinv  13419  grpidinv  13424  dfgrp3mlem  13463  issubg4m  13562  isnsg2  13572  elnmz  13577  ghmrn  13626  ghmnsgima  13637  srgideu  13767  ring1  13854  lringuplu  13991  subrgugrp  14035  isrrg  14058  islssm  14152  islssmg  14153  rnglidlmcl  14275  mplsubgfilemm  14493  mplsubgfilemcl  14494  basgen2  14586  bastop1  14588  iscn  14702  cnpval  14703  iscnp  14704  iscnp3  14708  cnprcl2k  14711  lmbr  14718  lmbr2  14719  lmbrf  14720  cnptoprest  14744  cnptoprest2  14745  cnmpt21  14796  ispsmet  14828  ismet  14849  isxmet  14850  metss  14999  qtopbasss  15026  cncfval  15077  elcncf2  15079  mulc1cncf  15094  cncfmet  15097  dedekindeulemloc  15124  dedekindeulemeu  15127  dedekindeu  15128  suplociccreex  15129  dedekindicclemloc  15133  dedekindicclemeu  15136  dedekindicclemicc  15137  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemloc  15146  ivthreinc  15150  dich0  15157  limccl  15164  ellimc3apf  15165  limcdifap  15167  limcmpted  15168  2irrexpqap  15483  perfectlem2  15505  2sqlem6  15630  2sqlem10  15635  bj-charfunbi  15784  bj-omtrans  15929  strcoll2  15956  strcollnfALT  15959  sscoll2  15961  2omap  15969  pw1nct  15977  0nninf  15978  nnsf  15979  peano4nninf  15980  nninfalllem1  15982  nninfself  15987  nninfsellemeq  15988  nninfsellemeqinf  15990  isomninnlem  16006  trilpolemlt1  16017  iswomninnlem  16025  iswomni0  16027  ismkvnnlem  16028  cndcap  16035  dceqnconst  16036  dcapnconst  16037  ltlenmkv  16046