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  4190  bnd2  4312  poeq1  4446  soeq1  4462  frforeq1  4490  frforeq3  4494  frirrg  4497  frind  4499  weeq1  4503  reusv3  4608  ontr2exmid  4674  reg2exmidlema  4683  posng  4849  ralxpf  4928  cnvpom  5333  funcnvuni  5453  fnmptfvd  5816  dff4im  5857  dff13f  5979  eusvobj2  6074  ovanraleqv  6112  ofreq  6309  caofdig  6340  uchoice  6375  suppssrst  6505  suppssrgst  6506  suppofss1dcl  6508  suppofss2dcl  6509  suppinisegdc  6513  smoeq  6566  recseq  6582  tfr0dm  6598  tfrlemiex  6607  tfr1onlemex  6623  tfr1onlemaccex  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemex  6636  tfrcllemaccex  6637  tfrcllemres  6638  elixp2  6990  pw2f1odclem  7140  xpf1o  7150  nneneq  7164  ac6sfi  7208  fimax2gtrilemstep  7211  fimax2gtri  7212  elssdc  7215  opabfi  7253  funisfsuppdc  7298  2omap  7324  supeq1  7332  supeq3  7336  supmoti  7339  eqsupti  7342  supubti  7345  suplubti  7346  supisoex  7355  cnvinfex  7364  eqinfti  7366  infvalti  7368  updjud  7428  ctssdclemr  7458  nninff  7468  nninfninc  7469  infnninf  7470  infnninfOLD  7471  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  enomnilem  7484  finomni  7486  exmidomni  7488  fodjuomnilemres  7494  ismkvnex  7501  fodjumkvlemres  7505  enmkvlem  7507  enwomnilem  7515  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemg  7521  nninfwlpoimlemdc  7523  exmidontriimlem3  7585  exmidontriim  7587  papeq1  7615  papsym  7618  papcotr  7619  tapeq1  7624  netap  7626  exmidapne  7632  cc2lem  7638  cc3  7640  elinp  7847  prloc  7864  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgpr  8055  caucvgprpr  8085  suplocexprlemloc  8094  suplocexpr  8098  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  caucvgsr  8175  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  lbreu  9283  sup3exmid  9295  nnsub  9352  indstr  10008  supinfneg  10010  infsupneg  10011  ublbneg  10028  lbzbi  10031  iccsupr  10384  zsupcllemstep  10678  infssuzex  10682  suprzubdc  10687  nninfdcex  10688  zsupssdc  10689  frecuzrdgsuc  10871  frecuzrdgg  10873  frecuzrdgsuctlem  10880  seq3f1olemstep  10971  seq3f1olemp  10972  seqfeq4g  10988  nn0ltexp2  11168  bccl  11226  hashfibc  11304  wrdind  11515  wrd2ind  11516  cau4  11904  caubnd2  11905  maxleast  12001  rexanre  12008  rexico  12009  fimaxre2  12015  fiidxsupcl  12017  minmax  12019  xrminmax  12055  clim  12071  clim2  12073  clim2c  12074  clim0c  12076  climabs0  12097  cn1lem  12104  sumeq1  12145  prodeq1f  12343  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlemex  12802  bezoutlemeu  12808  dfgcd3  12811  bezout  12812  dfgcd2  12815  nnwodc  12837  uzwodc  12838  nnwofdc  12839  sqrt2irr  12965  reumodprminv  13060  pc2dvds  13137  pcz  13139  prmpwdvds  13162  ballotfileme  13293  ennnfoneleminc  13359  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemnn0  13370  ennnfonelemr  13371  ennnfonelemim  13372  exmidunben  13374  ctinfomlemom  13375  ctinfom  13376  ctinf  13378  ctiunctlemudc  13385  ctiunct  13388  ssomct  13393  infpn2  13404  imasaddfnlemg  13693  mgm1  13748  sgrp1  13784  mhmima  13856  dfgrp2  13890  isgrpinv  13917  grpidinv  13922  dfgrp3mlem  13961  issubg4m  14054  isnsg2  14064  elnmz  14069  ghmrn  14118  ghmnsgima  14129  cntzex  14149  cntzfval  14151  elcntz  14153  resscntz  14165  srgideu  14382  ring1  14470  lringuplu  14611  subrgugrp  14656  isrrg  14679  islssm  14802  islssmg  14803  rnglidlmcl  14925  isassa  15110  psrbagmaxlem1  15178  psrbagmax  15183  basgen2  15324  bastop1  15326  iscn  15440  cnpval  15441  iscnp  15442  iscnp3  15446  cnprcl2k  15449  lmbr  15456  lmbr2  15457  lmbrf  15458  cnptoprest  15482  cnptoprest2  15483  cnmpt21  15534  ispsmet  15566  ismet  15587  isxmet  15588  metss  15737  qtopbasss  15764  cncfval  15815  elcncf2  15817  mulc1cncf  15832  cncfmet  15835  dedekindeulemloc  15862  dedekindeulemeu  15865  dedekindeu  15866  suplociccreex  15867  dedekindicclemloc  15871  dedekindicclemeu  15874  dedekindicclemicc  15875  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemloc  15884  ivthreinc  15888  dich0  15895  limccl  15902  ellimc3apf  15903  limcdifap  15905  limcmpted  15906  2irrexpqap  16231  zprmlogbaplem2  16233  zprmlogbap  16235  perfectlem2  16317  prmefexple  16325  bposlem1  16328  2sqlem6  16461  2sqlem10  16466  wksfval  16785  wlkvtxedg  16826  clwwlkg  16856  depind  16972  bj-charfunbi  17059  bj-omtrans  17204  strcoll2  17231  strcollnfALT  17234  sscoll2  17236  pw1nct  17255  exmidcon  17259  0nninf  17270  nnsf  17271  peano4nninf  17272  nninfalllem1  17274  nninfself  17279  nninfsellemeq  17280  nninfsellemeqinf  17282  isomninnlem  17302  rirrdisj  17308  trilpolemlt1  17314  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326  cndcap  17333  dceqnconst  17334  dcapnconst  17335  ltlenmkv  17344