Theorem ralbidv 2506

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  ralbii  2512  2ralbidv  2530  rexralbidv  2532  r19.32vdc  2655  raleqbi1dv  2714  raleqbidv  2718  cbvral2vw  2749  cbvral2v  2751  rspceaimv  2885  rspc2  2888  rspc3v  2893  reu6i  2964  reu7  2968  sbcralt  3075  sbcralg  3077  raaanlem  3565  2ralunsn  3839  elintg  3893  elintrabg  3898  eliin  3932  brralrspcev  4102  bnd2  4217  poeq1  4346  soeq1  4362  frforeq1  4390  frforeq3  4394  frirrg  4397  frind  4399  weeq1  4403  reusv3  4507  ontr2exmid  4573  reg2exmidlema  4582  posng  4747  ralxpf  4824  cnvpom  5225  funcnvuni  5343  fnmptfvd  5684  dff4im  5726  dff13f  5839  eusvobj2  5930  ovanraleqv  5968  ofreq  6162  caofdig  6192  uchoice  6223  smoeq  6376  recseq  6392  tfr0dm  6408  tfrlemiex  6417  tfr1onlemex  6433  tfr1onlemaccex  6434  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllemex  6446  tfrcllemaccex  6447  tfrcllemres  6448  elixp2  6789  pw2f1odclem  6931  xpf1o  6941  nneneq  6954  ac6sfi  6995  fimax2gtrilemstep  6997  fimax2gtri  6998  opabfi  7035  supeq1  7088  supeq3  7092  supmoti  7095  eqsupti  7098  supubti  7101  suplubti  7102  supisoex  7111  cnvinfex  7120  eqinfti  7122  infvalti  7124  updjud  7184  ctssdclemr  7214  nninff  7224  nninfninc  7225  infnninf  7226  infnninfOLD  7227  nnnninf  7228  nnnninfeq  7230  nnnninfeq2  7231  enomnilem  7240  finomni  7242  exmidomni  7244  fodjuomnilemres  7250  ismkvnex  7257  fodjumkvlemres  7261  enmkvlem  7263  enwomnilem  7271  nninfdcinf  7273  nninfwlporlem  7275  nninfwlpoimlemg  7277  nninfwlpoimlemdc  7279  exmidontriimlem3  7335  exmidontriim  7337  tapeq1  7364  netap  7366  exmidapne  7372  cc2lem  7378  cc3  7380  elinp  7587  prloc  7604  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgpr  7795  caucvgprpr  7825  suplocexprlemloc  7834  suplocexpr  7838  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  caucvgsr  7915  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  axcaucvglemcau  8011  axcaucvglemres  8012  axpre-suploclemres  8014  axpre-suploc  8015  lbreu  9018  sup3exmid  9030  nnsub  9075  indstr  9714  supinfneg  9716  infsupneg  9717  ublbneg  9734  lbzbi  9737  iccsupr  10088  zsupcllemstep  10372  infssuzex  10376  suprzubdc  10379  nninfdcex  10380  zsupssdc  10381  frecuzrdgsuc  10559  frecuzrdgg  10561  frecuzrdgsuctlem  10568  seq3f1olemstep  10659  seq3f1olemp  10660  seqfeq4g  10676  nn0ltexp2  10854  bccl  10912  cau4  11427  caubnd2  11428  maxleast  11524  rexanre  11531  rexico  11532  fimaxre2  11538  minmax  11541  xrminmax  11576  clim  11592  clim2  11594  clim2c  11595  clim0c  11597  climabs0  11618  cn1lem  11625  sumeq1  11666  prodeq1f  11863  bezoutlemstep  12318  bezoutlemmain  12319  bezoutlemex  12322  bezoutlemeu  12328  dfgcd3  12331  bezout  12332  dfgcd2  12335  nnwodc  12357  uzwodc  12358  nnwofdc  12359  sqrt2irr  12484  reumodprminv  12576  pc2dvds  12653  pcz  12655  prmpwdvds  12678  ennnfoneleminc  12782  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemnn0  12793  ennnfonelemr  12794  ennnfonelemim  12795  exmidunben  12797  ctinfomlemom  12798  ctinfom  12799  ctinf  12801  ctiunctlemudc  12808  ctiunct  12811  ssomct  12816  infpn2  12827  imasaddfnlemg  13146  mgm1  13202  sgrp1  13243  mhmima  13323  dfgrp2  13359  isgrpinv  13386  grpidinv  13391  dfgrp3mlem  13430  issubg4m  13529  isnsg2  13539  elnmz  13544  ghmrn  13593  ghmnsgima  13604  srgideu  13734  ring1  13821  lringuplu  13958  subrgugrp  14002  isrrg  14025  islssm  14119  islssmg  14120  rnglidlmcl  14242  mplsubgfilemm  14460  mplsubgfilemcl  14461  basgen2  14553  bastop1  14555  iscn  14669  cnpval  14670  iscnp  14671  iscnp3  14675  cnprcl2k  14678  lmbr  14685  lmbr2  14686  lmbrf  14687  cnptoprest  14711  cnptoprest2  14712  cnmpt21  14763  ispsmet  14795  ismet  14816  isxmet  14817  metss  14966  qtopbasss  14993  cncfval  15044  elcncf2  15046  mulc1cncf  15061  cncfmet  15064  dedekindeulemloc  15091  dedekindeulemeu  15094  dedekindeu  15095  suplociccreex  15096  dedekindicclemloc  15100  dedekindicclemeu  15103  dedekindicclemicc  15104  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemloc  15113  ivthreinc  15117  dich0  15124  limccl  15131  ellimc3apf  15132  limcdifap  15134  limcmpted  15135  2irrexpqap  15450  perfectlem2  15472  2sqlem6  15597  2sqlem10  15602  bj-charfunbi  15747  bj-omtrans  15892  strcoll2  15919  strcollnfALT  15922  sscoll2  15924  2omap  15932  pw1nct  15940  0nninf  15941  nnsf  15942  peano4nninf  15943  nninfalllem1  15945  nninfself  15950  nninfsellemeq  15951  nninfsellemeqinf  15953  isomninnlem  15969  trilpolemlt1  15980  iswomninnlem  15988  iswomni0  15990  ismkvnnlem  15991  cndcap  15998  dceqnconst  15999  dcapnconst  16000  ltlenmkv  16009