Theorem ralbidv 2550

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralbii  2556  2ralbidv  2574  rexralbidv  2576  r19.32vdc  2700  raleqbi1dv  2761  raleqbidv  2765  cbvral2vw  2797  cbvral2v  2799  rspceaimv  2938  rspc2  2941  rspc3v  2946  reu6i  3017  reu7  3021  sbcralt  3128  sbcralg  3130  reu8nf  3133  raaanlem  3632  2ralunsn  3924  elintg  3978  elintrabg  3983  eliin  4017  brralrspcev  4189  bnd2  4310  poeq1  4444  soeq1  4460  frforeq1  4488  frforeq3  4492  frirrg  4495  frind  4497  weeq1  4501  reusv3  4606  ontr2exmid  4672  reg2exmidlema  4681  posng  4847  ralxpf  4926  cnvpom  5330  funcnvuni  5450  fnmptfvd  5813  dff4im  5854  dff13f  5976  eusvobj2  6071  ovanraleqv  6109  ofreq  6306  caofdig  6336  uchoice  6371  suppssrst  6501  suppssrgst  6502  suppofss1dcl  6504  suppofss2dcl  6505  smoeq  6561  recseq  6577  tfr0dm  6593  tfrlemiex  6602  tfr1onlemex  6618  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  elixp2  6984  pw2f1odclem  7134  xpf1o  7144  nneneq  7158  ac6sfi  7202  fimax2gtrilemstep  7205  fimax2gtri  7206  elssdc  7209  opabfi  7247  2omap  7319  supeq1  7327  supeq3  7331  supmoti  7334  eqsupti  7337  supubti  7340  suplubti  7341  supisoex  7350  cnvinfex  7359  eqinfti  7361  infvalti  7363  updjud  7423  ctssdclemr  7453  nninff  7463  nninfninc  7464  infnninf  7465  infnninfOLD  7466  nnnninf  7467  nnnninfeq  7469  nnnninfeq2  7470  enomnilem  7479  finomni  7481  exmidomni  7483  fodjuomnilemres  7489  ismkvnex  7496  fodjumkvlemres  7500  enmkvlem  7502  enwomnilem  7510  nninfdcinf  7512  nninfwlporlem  7514  nninfwlpoimlemg  7516  nninfwlpoimlemdc  7518  exmidontriimlem3  7580  exmidontriim  7582  papeq1  7610  papsym  7613  papcotr  7614  tapeq1  7619  netap  7621  exmidapne  7627  cc2lem  7633  cc3  7635  elinp  7842  prloc  7859  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgpr  8050  caucvgprpr  8080  suplocexprlemloc  8089  suplocexpr  8093  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  caucvgsr  8170  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  lbreu  9278  sup3exmid  9290  nnsub  9346  indstr  10003  supinfneg  10005  infsupneg  10006  ublbneg  10023  lbzbi  10026  iccsupr  10379  zsupcllemstep  10673  infssuzex  10677  suprzubdc  10682  nninfdcex  10683  zsupssdc  10684  frecuzrdgsuc  10866  frecuzrdgg  10868  frecuzrdgsuctlem  10875  seq3f1olemstep  10966  seq3f1olemp  10967  seqfeq4g  10983  nn0ltexp2  11163  bccl  11221  hashfibc  11299  wrdind  11510  wrd2ind  11511  cau4  11899  caubnd2  11900  maxleast  11996  rexanre  12003  rexico  12004  fimaxre2  12010  fiidxsupcl  12012  minmax  12014  xrminmax  12050  clim  12066  clim2  12068  clim2c  12069  clim0c  12071  climabs0  12092  cn1lem  12099  sumeq1  12140  prodeq1f  12338  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlemex  12797  bezoutlemeu  12803  dfgcd3  12806  bezout  12807  dfgcd2  12810  nnwodc  12832  uzwodc  12833  nnwofdc  12834  sqrt2irr  12960  reumodprminv  13055  pc2dvds  13132  pcz  13134  prmpwdvds  13157  ballotfileme  13288  ennnfoneleminc  13354  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemnn0  13365  ennnfonelemr  13366  ennnfonelemim  13367  exmidunben  13369  ctinfomlemom  13370  ctinfom  13371  ctinf  13373  ctiunctlemudc  13380  ctiunct  13383  ssomct  13388  infpn2  13399  imasaddfnlemg  13688  mgm1  13743  sgrp1  13779  mhmima  13851  dfgrp2  13885  isgrpinv  13912  grpidinv  13917  dfgrp3mlem  13956  issubg4m  14049  isnsg2  14059  elnmz  14064  ghmrn  14113  ghmnsgima  14124  cntzex  14144  cntzfval  14146  elcntz  14148  resscntz  14160  srgideu  14360  ring1  14448  lringuplu  14587  subrgugrp  14632  isrrg  14655  islssm  14778  islssmg  14779  rnglidlmcl  14901  isassa  15086  mplsubgfilemm  15180  mplsubgfilemcl  15181  basgen2  15273  bastop1  15275  iscn  15389  cnpval  15390  iscnp  15391  iscnp3  15395  cnprcl2k  15398  lmbr  15405  lmbr2  15406  lmbrf  15407  cnptoprest  15431  cnptoprest2  15432  cnmpt21  15483  ispsmet  15515  ismet  15536  isxmet  15537  metss  15686  qtopbasss  15713  cncfval  15764  elcncf2  15766  mulc1cncf  15781  cncfmet  15784  dedekindeulemloc  15811  dedekindeulemeu  15814  dedekindeu  15815  suplociccreex  15816  dedekindicclemloc  15820  dedekindicclemeu  15823  dedekindicclemicc  15824  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemloc  15833  ivthreinc  15837  dich0  15844  limccl  15851  ellimc3apf  15852  limcdifap  15854  limcmpted  15855  2irrexpqap  16175  zprmlogbaplem2  16177  zprmlogbap  16179  perfectlem2  16261  prmefexple  16269  bposlem1  16272  2sqlem6  16405  2sqlem10  16410  wksfval  16729  wlkvtxedg  16770  clwwlkg  16800  depind  16916  bj-charfunbi  17003  bj-omtrans  17148  strcoll2  17175  strcollnfALT  17178  sscoll2  17180  pw1nct  17199  exmidcon  17203  0nninf  17213  nnsf  17214  peano4nninf  17215  nninfalllem1  17217  nninfself  17222  nninfsellemeq  17223  nninfsellemeqinf  17225  isomninnlem  17245  rirrdisj  17251  trilpolemlt1  17257  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269  cndcap  17276  dceqnconst  17277  dcapnconst  17278  ltlenmkv  17287