Theorem ralbidv 2494

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  ralbii  2500  2ralbidv  2518  rexralbidv  2520  r19.32vdc  2643  raleqbi1dv  2702  raleqbidv  2706  cbvral2vw  2737  cbvral2v  2739  rspceaimv  2872  rspc2  2875  rspc3v  2880  reu6i  2951  reu7  2955  sbcralt  3062  sbcralg  3064  raaanlem  3551  2ralunsn  3824  elintg  3878  elintrabg  3883  eliin  3917  brralrspcev  4087  bnd2  4202  poeq1  4330  soeq1  4346  frforeq1  4374  frforeq3  4378  frirrg  4381  frind  4383  weeq1  4387  reusv3  4491  ontr2exmid  4557  reg2exmidlema  4566  posng  4731  ralxpf  4808  cnvpom  5208  funcnvuni  5323  fnmptfvd  5662  dff4im  5704  dff13f  5813  eusvobj2  5904  ovanraleqv  5942  ofreq  6134  caofdig  6159  uchoice  6190  smoeq  6343  recseq  6359  tfr0dm  6375  tfrlemiex  6384  tfr1onlemex  6400  tfr1onlemaccex  6401  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllemex  6413  tfrcllemaccex  6414  tfrcllemres  6415  elixp2  6756  pw2f1odclem  6890  xpf1o  6900  nneneq  6913  ac6sfi  6954  fimax2gtrilemstep  6956  fimax2gtri  6957  opabfi  6992  supeq1  7045  supeq3  7049  supmoti  7052  eqsupti  7055  supubti  7058  suplubti  7059  supisoex  7068  cnvinfex  7077  eqinfti  7079  infvalti  7081  updjud  7141  ctssdclemr  7171  nninff  7181  nninfninc  7182  infnninf  7183  infnninfOLD  7184  nnnninf  7185  nnnninfeq  7187  nnnninfeq2  7188  enomnilem  7197  finomni  7199  exmidomni  7201  fodjuomnilemres  7207  ismkvnex  7214  fodjumkvlemres  7218  enmkvlem  7220  enwomnilem  7228  nninfdcinf  7230  nninfwlporlem  7232  nninfwlpoimlemg  7234  nninfwlpoimlemdc  7236  exmidontriimlem3  7283  exmidontriim  7285  tapeq1  7312  netap  7314  exmidapne  7320  cc2lem  7326  cc3  7328  elinp  7534  prloc  7551  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgpr  7742  caucvgprpr  7772  suplocexprlemloc  7781  suplocexpr  7785  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  caucvgsr  7862  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  axcaucvglemcau  7958  axcaucvglemres  7959  axpre-suploclemres  7961  axpre-suploc  7962  lbreu  8964  sup3exmid  8976  nnsub  9021  indstr  9658  supinfneg  9660  infsupneg  9661  ublbneg  9678  lbzbi  9681  iccsupr  10032  frecuzrdgsuc  10485  frecuzrdgg  10487  frecuzrdgsuctlem  10494  seq3f1olemstep  10585  seq3f1olemp  10586  seqfeq4g  10602  nn0ltexp2  10780  bccl  10838  cau4  11260  caubnd2  11261  maxleast  11357  rexanre  11364  rexico  11365  fimaxre2  11370  minmax  11373  xrminmax  11408  clim  11424  clim2  11426  clim2c  11427  clim0c  11429  climabs0  11450  cn1lem  11457  sumeq1  11498  prodeq1f  11695  zsupcllemstep  12082  infssuzex  12086  suprzubdc  12089  nninfdcex  12090  zsupssdc  12091  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemex  12138  bezoutlemeu  12144  dfgcd3  12147  bezout  12148  dfgcd2  12151  nnwodc  12173  uzwodc  12174  nnwofdc  12175  sqrt2irr  12300  reumodprminv  12391  pc2dvds  12468  pcz  12470  prmpwdvds  12493  ennnfoneleminc  12568  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemnn0  12579  ennnfonelemr  12580  ennnfonelemim  12581  exmidunben  12583  ctinfomlemom  12584  ctinfom  12585  ctinf  12587  ctiunctlemudc  12594  ctiunct  12597  ssomct  12602  infpn2  12613  imasaddfnlemg  12897  mgm1  12953  sgrp1  12994  mhmima  13063  dfgrp2  13099  isgrpinv  13126  grpidinv  13131  dfgrp3mlem  13170  issubg4m  13263  isnsg2  13273  elnmz  13278  ghmrn  13327  ghmnsgima  13338  srgideu  13468  ring1  13555  lringuplu  13692  subrgugrp  13736  isrrg  13759  islssm  13853  islssmg  13854  rnglidlmcl  13976  basgen2  14249  bastop1  14251  iscn  14365  cnpval  14366  iscnp  14367  iscnp3  14371  cnprcl2k  14374  lmbr  14381  lmbr2  14382  lmbrf  14383  cnptoprest  14407  cnptoprest2  14408  cnmpt21  14459  ispsmet  14491  ismet  14512  isxmet  14513  metss  14662  qtopbasss  14689  cncfval  14727  elcncf2  14729  mulc1cncf  14744  cncfmet  14747  dedekindeulemloc  14773  dedekindeulemeu  14776  dedekindeu  14777  suplociccreex  14778  dedekindicclemloc  14782  dedekindicclemeu  14785  dedekindicclemicc  14786  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemloc  14795  ivthreinc  14799  dich0  14806  limccl  14813  ellimc3apf  14814  limcdifap  14816  limcmpted  14817  2irrexpqap  15110  2sqlem6  15207  2sqlem10  15212  bj-charfunbi  15303  bj-omtrans  15448  strcoll2  15475  strcollnfALT  15478  sscoll2  15480  pw1nct  15493  0nninf  15494  nnsf  15495  peano4nninf  15496  nninfalllem1  15498  nninfself  15503  nninfsellemeq  15504  nninfsellemeqinf  15506  isomninnlem  15520  trilpolemlt1  15531  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542  cndcap  15549  dceqnconst  15550  dcapnconst  15551  ltlenmkv  15560