Theorem ralbidv 2530

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralbii  2536  2ralbidv  2554  rexralbidv  2556  r19.32vdc  2680  raleqbi1dv  2740  raleqbidv  2744  cbvral2vw  2776  cbvral2v  2778  rspceaimv  2915  rspc2  2918  rspc3v  2923  reu6i  2994  reu7  2998  sbcralt  3105  sbcralg  3107  reu8nf  3110  raaanlem  3596  2ralunsn  3877  elintg  3931  elintrabg  3936  eliin  3970  brralrspcev  4142  bnd2  4257  poeq1  4390  soeq1  4406  frforeq1  4434  frforeq3  4438  frirrg  4441  frind  4443  weeq1  4447  reusv3  4551  ontr2exmid  4617  reg2exmidlema  4626  posng  4791  ralxpf  4868  cnvpom  5271  funcnvuni  5390  fnmptfvd  5741  dff4im  5783  dff13f  5900  eusvobj2  5993  ovanraleqv  6031  ofreq  6228  caofdig  6258  uchoice  6289  smoeq  6442  recseq  6458  tfr0dm  6474  tfrlemiex  6483  tfr1onlemex  6499  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  elixp2  6857  pw2f1odclem  7003  xpf1o  7013  nneneq  7026  ac6sfi  7068  fimax2gtrilemstep  7070  fimax2gtri  7071  opabfi  7108  supeq1  7161  supeq3  7165  supmoti  7168  eqsupti  7171  supubti  7174  suplubti  7175  supisoex  7184  cnvinfex  7193  eqinfti  7195  infvalti  7197  updjud  7257  ctssdclemr  7287  nninff  7297  nninfninc  7298  infnninf  7299  infnninfOLD  7300  nnnninf  7301  nnnninfeq  7303  nnnninfeq2  7304  enomnilem  7313  finomni  7315  exmidomni  7317  fodjuomnilemres  7323  ismkvnex  7330  fodjumkvlemres  7334  enmkvlem  7336  enwomnilem  7344  nninfdcinf  7346  nninfwlporlem  7348  nninfwlpoimlemg  7350  nninfwlpoimlemdc  7352  exmidontriimlem3  7413  exmidontriim  7415  tapeq1  7446  netap  7448  exmidapne  7454  cc2lem  7460  cc3  7462  elinp  7669  prloc  7686  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  caucvgpr  7877  caucvgprpr  7907  suplocexprlemloc  7916  suplocexpr  7920  caucvgsrlemgt1  7990  caucvgsrlemoffres  7995  caucvgsr  7997  suplocsrlemb  8001  suplocsrlempr  8002  suplocsrlem  8003  axcaucvglemcau  8093  axcaucvglemres  8094  axpre-suploclemres  8096  axpre-suploc  8097  lbreu  9100  sup3exmid  9112  nnsub  9157  indstr  9796  supinfneg  9798  infsupneg  9799  ublbneg  9816  lbzbi  9819  iccsupr  10170  zsupcllemstep  10457  infssuzex  10461  suprzubdc  10464  nninfdcex  10465  zsupssdc  10466  frecuzrdgsuc  10644  frecuzrdgg  10646  frecuzrdgsuctlem  10653  seq3f1olemstep  10744  seq3f1olemp  10745  seqfeq4g  10761  nn0ltexp2  10939  bccl  10997  wrdind  11262  wrd2ind  11263  cau4  11635  caubnd2  11636  maxleast  11732  rexanre  11739  rexico  11740  fimaxre2  11746  minmax  11749  xrminmax  11784  clim  11800  clim2  11802  clim2c  11803  clim0c  11805  climabs0  11826  cn1lem  11833  sumeq1  11874  prodeq1f  12071  bezoutlemstep  12526  bezoutlemmain  12527  bezoutlemex  12530  bezoutlemeu  12536  dfgcd3  12539  bezout  12540  dfgcd2  12543  nnwodc  12565  uzwodc  12566  nnwofdc  12567  sqrt2irr  12692  reumodprminv  12784  pc2dvds  12861  pcz  12863  prmpwdvds  12886  ennnfoneleminc  12990  ennnfonelemex  12993  ennnfonelemhom  12994  ennnfonelemnn0  13001  ennnfonelemr  13002  ennnfonelemim  13003  exmidunben  13005  ctinfomlemom  13006  ctinfom  13007  ctinf  13009  ctiunctlemudc  13016  ctiunct  13019  ssomct  13024  infpn2  13035  imasaddfnlemg  13355  mgm1  13411  sgrp1  13452  mhmima  13532  dfgrp2  13568  isgrpinv  13595  grpidinv  13600  dfgrp3mlem  13639  issubg4m  13738  isnsg2  13748  elnmz  13753  ghmrn  13802  ghmnsgima  13813  srgideu  13943  ring1  14030  lringuplu  14168  subrgugrp  14212  isrrg  14235  islssm  14329  islssmg  14330  rnglidlmcl  14452  mplsubgfilemm  14670  mplsubgfilemcl  14671  basgen2  14763  bastop1  14765  iscn  14879  cnpval  14880  iscnp  14881  iscnp3  14885  cnprcl2k  14888  lmbr  14895  lmbr2  14896  lmbrf  14897  cnptoprest  14921  cnptoprest2  14922  cnmpt21  14973  ispsmet  15005  ismet  15026  isxmet  15027  metss  15176  qtopbasss  15203  cncfval  15254  elcncf2  15256  mulc1cncf  15271  cncfmet  15274  dedekindeulemloc  15301  dedekindeulemeu  15304  dedekindeu  15305  suplociccreex  15306  dedekindicclemloc  15310  dedekindicclemeu  15313  dedekindicclemicc  15314  ivthinclemlopn  15318  ivthinclemlr  15319  ivthinclemuopn  15320  ivthinclemur  15321  ivthinclemloc  15323  ivthreinc  15327  dich0  15334  limccl  15341  ellimc3apf  15342  limcdifap  15344  limcmpted  15345  2irrexpqap  15660  perfectlem2  15682  2sqlem6  15807  2sqlem10  15812  wksfval  16043  wlkvtxedg  16084  bj-charfunbi  16198  bj-omtrans  16343  strcoll2  16370  strcollnfALT  16373  sscoll2  16375  2omap  16385  pw1nct  16395  0nninf  16397  nnsf  16398  peano4nninf  16399  nninfalllem1  16401  nninfself  16406  nninfsellemeq  16407  nninfsellemeqinf  16409  isomninnlem  16425  trilpolemlt1  16436  iswomninnlem  16444  iswomni0  16446  ismkvnnlem  16447  cndcap  16454  dceqnconst  16455  dcapnconst  16456  ltlenmkv  16465