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 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

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

This theorem is referenced 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  3629  2ralunsn  3919  elintg  3973  elintrabg  3978  eliin  4012  brralrspcev  4184  bnd2  4305  poeq1  4439  soeq1  4455  frforeq1  4483  frforeq3  4487  frirrg  4490  frind  4492  weeq1  4496  reusv3  4601  ontr2exmid  4667  reg2exmidlema  4676  posng  4842  ralxpf  4921  cnvpom  5325  funcnvuni  5445  fnmptfvd  5804  dff4im  5845  dff13f  5966  eusvobj2  6061  ovanraleqv  6099  ofreq  6296  caofdig  6326  uchoice  6361  suppssrst  6491  suppssrgst  6492  suppofss1dcl  6494  suppofss2dcl  6495  smoeq  6551  recseq  6567  tfr0dm  6583  tfrlemiex  6592  tfr1onlemex  6608  tfr1onlemaccex  6609  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllemex  6621  tfrcllemaccex  6622  tfrcllemres  6623  elixp2  6974  pw2f1odclem  7124  xpf1o  7134  nneneq  7148  ac6sfi  7192  fimax2gtrilemstep  7195  fimax2gtri  7196  elssdc  7199  opabfi  7237  2omap  7308  supeq1  7316  supeq3  7320  supmoti  7323  eqsupti  7326  supubti  7329  suplubti  7330  supisoex  7339  cnvinfex  7348  eqinfti  7350  infvalti  7352  updjud  7412  ctssdclemr  7442  nninff  7452  nninfninc  7453  infnninf  7454  infnninfOLD  7455  nnnninf  7456  nnnninfeq  7458  nnnninfeq2  7459  enomnilem  7468  finomni  7470  exmidomni  7472  fodjuomnilemres  7478  ismkvnex  7485  fodjumkvlemres  7489  enmkvlem  7491  enwomnilem  7499  nninfdcinf  7501  nninfwlporlem  7503  nninfwlpoimlemg  7505  nninfwlpoimlemdc  7507  exmidontriimlem3  7569  exmidontriim  7571  papeq1  7599  papsym  7602  papcotr  7603  tapeq1  7608  netap  7610  exmidapne  7616  cc2lem  7622  cc3  7624  elinp  7831  prloc  7848  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgpr  8039  caucvgprpr  8069  suplocexprlemloc  8078  suplocexpr  8082  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  caucvgsr  8159  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  axcaucvglemcau  8255  axcaucvglemres  8256  axpre-suploclemres  8258  axpre-suploc  8259  lbreu  9265  sup3exmid  9277  nnsub  9322  indstr  9972  supinfneg  9974  infsupneg  9975  ublbneg  9992  lbzbi  9995  iccsupr  10347  zsupcllemstep  10640  infssuzex  10644  suprzubdc  10649  nninfdcex  10650  zsupssdc  10651  frecuzrdgsuc  10829  frecuzrdgg  10831  frecuzrdgsuctlem  10838  seq3f1olemstep  10929  seq3f1olemp  10930  seqfeq4g  10946  nn0ltexp2  11125  bccl  11183  hashfibc  11261  wrdind  11472  wrd2ind  11473  cau4  11860  caubnd2  11861  maxleast  11957  rexanre  11964  rexico  11965  fimaxre2  11971  minmax  11974  xrminmax  12009  clim  12025  clim2  12027  clim2c  12028  clim0c  12030  climabs0  12051  cn1lem  12058  sumeq1  12099  prodeq1f  12297  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlemex  12756  bezoutlemeu  12762  dfgcd3  12765  bezout  12766  dfgcd2  12769  nnwodc  12791  uzwodc  12792  nnwofdc  12793  sqrt2irr  12918  reumodprminv  13010  pc2dvds  13087  pcz  13089  prmpwdvds  13112  ballotfileme  13214  ennnfoneleminc  13280  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemnn0  13291  ennnfonelemr  13292  ennnfonelemim  13293  exmidunben  13295  ctinfomlemom  13296  ctinfom  13297  ctinf  13299  ctiunctlemudc  13306  ctiunct  13309  ssomct  13314  infpn2  13325  imasaddfnlemg  13612  mgm1  13667  sgrp1  13703  mhmima  13775  dfgrp2  13809  isgrpinv  13836  grpidinv  13841  dfgrp3mlem  13880  issubg4m  13973  isnsg2  13983  elnmz  13988  ghmrn  14037  ghmnsgima  14048  srgideu  14250  ring1  14337  lringuplu  14476  subrgugrp  14521  isrrg  14544  islssm  14666  islssmg  14667  rnglidlmcl  14789  mplsubgfilemm  15012  mplsubgfilemcl  15013  basgen2  15105  bastop1  15107  iscn  15221  cnpval  15222  iscnp  15223  iscnp3  15227  cnprcl2k  15230  lmbr  15237  lmbr2  15238  lmbrf  15239  cnptoprest  15263  cnptoprest2  15264  cnmpt21  15315  ispsmet  15347  ismet  15368  isxmet  15369  metss  15518  qtopbasss  15545  cncfval  15596  elcncf2  15598  mulc1cncf  15613  cncfmet  15616  dedekindeulemloc  15643  dedekindeulemeu  15646  dedekindeu  15647  suplociccreex  15648  dedekindicclemloc  15652  dedekindicclemeu  15655  dedekindicclemicc  15656  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemloc  15665  ivthreinc  15669  dich0  15676  limccl  15683  ellimc3apf  15684  limcdifap  15686  limcmpted  15687  2irrexpqap  16003  perfectlem2  16028  2sqlem6  16153  2sqlem10  16158  wksfval  16477  wlkvtxedg  16518  clwwlkg  16548  depind  16664  bj-charfunbi  16751  bj-omtrans  16896  strcoll2  16923  strcollnfALT  16926  sscoll2  16928  pw1nct  16947  exmidcon  16950  0nninf  16952  nnsf  16953  peano4nninf  16954  nninfalllem1  16956  nninfself  16961  nninfsellemeq  16962  nninfsellemeqinf  16964  isomninnlem  16984  trilpolemlt1  16995  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007  cndcap  17014  dceqnconst  17015  dcapnconst  17016  ltlenmkv  17025