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  7318  supeq1  7326  supeq3  7330  supmoti  7333  eqsupti  7336  supubti  7339  suplubti  7340  supisoex  7349  cnvinfex  7358  eqinfti  7360  infvalti  7362  updjud  7422  ctssdclemr  7452  nninff  7462  nninfninc  7463  infnninf  7464  infnninfOLD  7465  nnnninf  7466  nnnninfeq  7468  nnnninfeq2  7469  enomnilem  7478  finomni  7480  exmidomni  7482  fodjuomnilemres  7488  ismkvnex  7495  fodjumkvlemres  7499  enmkvlem  7501  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemg  7515  nninfwlpoimlemdc  7517  exmidontriimlem3  7579  exmidontriim  7581  papeq1  7609  papsym  7612  papcotr  7613  tapeq1  7618  netap  7620  exmidapne  7626  cc2lem  7632  cc3  7634  elinp  7841  prloc  7858  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgpr  8049  caucvgprpr  8079  suplocexprlemloc  8088  suplocexpr  8092  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  lbreu  9275  sup3exmid  9287  nnsub  9343  indstr  9993  supinfneg  9995  infsupneg  9996  ublbneg  10013  lbzbi  10016  iccsupr  10368  zsupcllemstep  10662  infssuzex  10666  suprzubdc  10671  nninfdcex  10672  zsupssdc  10673  frecuzrdgsuc  10851  frecuzrdgg  10853  frecuzrdgsuctlem  10860  seq3f1olemstep  10951  seq3f1olemp  10952  seqfeq4g  10968  nn0ltexp2  11147  bccl  11205  hashfibc  11283  wrdind  11494  wrd2ind  11495  cau4  11882  caubnd2  11883  maxleast  11979  rexanre  11986  rexico  11987  fimaxre2  11993  minmax  11996  xrminmax  12031  clim  12047  clim2  12049  clim2c  12050  clim0c  12052  climabs0  12073  cn1lem  12080  sumeq1  12121  prodeq1f  12319  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemex  12778  bezoutlemeu  12784  dfgcd3  12787  bezout  12788  dfgcd2  12791  nnwodc  12813  uzwodc  12814  nnwofdc  12815  sqrt2irr  12940  reumodprminv  13032  pc2dvds  13109  pcz  13111  prmpwdvds  13134  ballotfileme  13236  ennnfoneleminc  13302  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemnn0  13313  ennnfonelemr  13314  ennnfonelemim  13315  exmidunben  13317  ctinfomlemom  13318  ctinfom  13319  ctinf  13321  ctiunctlemudc  13328  ctiunct  13331  ssomct  13336  infpn2  13347  imasaddfnlemg  13635  mgm1  13690  sgrp1  13726  mhmima  13798  dfgrp2  13832  isgrpinv  13859  grpidinv  13864  dfgrp3mlem  13903  issubg4m  13996  isnsg2  14006  elnmz  14011  ghmrn  14060  ghmnsgima  14071  srgideu  14276  ring1  14364  lringuplu  14503  subrgugrp  14548  isrrg  14571  islssm  14694  islssmg  14695  rnglidlmcl  14817  isassa  15002  mplsubgfilemm  15089  mplsubgfilemcl  15090  basgen2  15182  bastop1  15184  iscn  15298  cnpval  15299  iscnp  15300  iscnp3  15304  cnprcl2k  15307  lmbr  15314  lmbr2  15315  lmbrf  15316  cnptoprest  15340  cnptoprest2  15341  cnmpt21  15392  ispsmet  15424  ismet  15445  isxmet  15446  metss  15595  qtopbasss  15622  cncfval  15673  elcncf2  15675  mulc1cncf  15690  cncfmet  15693  dedekindeulemloc  15720  dedekindeulemeu  15723  dedekindeu  15724  suplociccreex  15725  dedekindicclemloc  15729  dedekindicclemeu  15732  dedekindicclemicc  15733  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemloc  15742  ivthreinc  15746  dich0  15753  limccl  15760  ellimc3apf  15761  limcdifap  15763  limcmpted  15764  2irrexpqap  16080  perfectlem2  16114  2sqlem6  16239  2sqlem10  16244  wksfval  16563  wlkvtxedg  16604  clwwlkg  16634  depind  16750  bj-charfunbi  16837  bj-omtrans  16982  strcoll2  17009  strcollnfALT  17012  sscoll2  17014  pw1nct  17033  exmidcon  17037  0nninf  17047  nnsf  17048  peano4nninf  17049  nninfalllem1  17051  nninfself  17056  nninfsellemeq  17057  nninfsellemeqinf  17059  isomninnlem  17079  trilpolemlt1  17090  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102  cndcap  17109  dceqnconst  17110  dcapnconst  17111  ltlenmkv  17120