Theorem ralbidv 2530

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralbii  2536  2ralbidv  2554  rexralbidv  2556  r19.32vdc  2680  raleqbi1dv  2740  raleqbidv  2744  cbvral2vw  2776  cbvral2v  2778  rspceaimv  2915  rspc2  2918  rspc3v  2923  reu6i  2994  reu7  2998  sbcralt  3105  sbcralg  3107  reu8nf  3110  raaanlem  3596  2ralunsn  3877  elintg  3931  elintrabg  3936  eliin  3970  brralrspcev  4142  bnd2  4257  poeq1  4390  soeq1  4406  frforeq1  4434  frforeq3  4438  frirrg  4441  frind  4443  weeq1  4447  reusv3  4551  ontr2exmid  4617  reg2exmidlema  4626  posng  4791  ralxpf  4868  cnvpom  5271  funcnvuni  5390  fnmptfvd  5741  dff4im  5783  dff13f  5900  eusvobj2  5993  ovanraleqv  6031  ofreq  6228  caofdig  6258  uchoice  6289  smoeq  6442  recseq  6458  tfr0dm  6474  tfrlemiex  6483  tfr1onlemex  6499  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  elixp2  6857  pw2f1odclem  7003  xpf1o  7013  nneneq  7026  ac6sfi  7068  fimax2gtrilemstep  7071  fimax2gtri  7072  elssdc  7075  opabfi  7111  supeq1  7164  supeq3  7168  supmoti  7171  eqsupti  7174  supubti  7177  suplubti  7178  supisoex  7187  cnvinfex  7196  eqinfti  7198  infvalti  7200  updjud  7260  ctssdclemr  7290  nninff  7300  nninfninc  7301  infnninf  7302  infnninfOLD  7303  nnnninf  7304  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  finomni  7318  exmidomni  7320  fodjuomnilemres  7326  ismkvnex  7333  fodjumkvlemres  7337  enmkvlem  7339  enwomnilem  7347  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemg  7353  nninfwlpoimlemdc  7355  exmidontriimlem3  7416  exmidontriim  7418  tapeq1  7449  netap  7451  exmidapne  7457  cc2lem  7463  cc3  7465  elinp  7672  prloc  7689  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgpr  7880  caucvgprpr  7910  suplocexprlemloc  7919  suplocexpr  7923  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  caucvgsr  8000  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  axpre-suploc  8100  lbreu  9103  sup3exmid  9115  nnsub  9160  indstr  9800  supinfneg  9802  infsupneg  9803  ublbneg  9820  lbzbi  9823  iccsupr  10174  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  nninfdcex  10469  zsupssdc  10470  frecuzrdgsuc  10648  frecuzrdgg  10650  frecuzrdgsuctlem  10657  seq3f1olemstep  10748  seq3f1olemp  10749  seqfeq4g  10765  nn0ltexp2  10943  bccl  11001  wrdind  11270  wrd2ind  11271  cau4  11643  caubnd2  11644  maxleast  11740  rexanre  11747  rexico  11748  fimaxre2  11754  minmax  11757  xrminmax  11792  clim  11808  clim2  11810  clim2c  11811  clim0c  11813  climabs0  11834  cn1lem  11841  sumeq1  11882  prodeq1f  12079  bezoutlemstep  12534  bezoutlemmain  12535  bezoutlemex  12538  bezoutlemeu  12544  dfgcd3  12547  bezout  12548  dfgcd2  12551  nnwodc  12573  uzwodc  12574  nnwofdc  12575  sqrt2irr  12700  reumodprminv  12792  pc2dvds  12869  pcz  12871  prmpwdvds  12894  ennnfoneleminc  12998  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemnn0  13009  ennnfonelemr  13010  ennnfonelemim  13011  exmidunben  13013  ctinfomlemom  13014  ctinfom  13015  ctinf  13017  ctiunctlemudc  13024  ctiunct  13027  ssomct  13032  infpn2  13043  imasaddfnlemg  13363  mgm1  13419  sgrp1  13460  mhmima  13540  dfgrp2  13576  isgrpinv  13603  grpidinv  13608  dfgrp3mlem  13647  issubg4m  13746  isnsg2  13756  elnmz  13761  ghmrn  13810  ghmnsgima  13821  srgideu  13951  ring1  14038  lringuplu  14176  subrgugrp  14220  isrrg  14243  islssm  14337  islssmg  14338  rnglidlmcl  14460  mplsubgfilemm  14678  mplsubgfilemcl  14679  basgen2  14771  bastop1  14773  iscn  14887  cnpval  14888  iscnp  14889  iscnp3  14893  cnprcl2k  14896  lmbr  14903  lmbr2  14904  lmbrf  14905  cnptoprest  14929  cnptoprest2  14930  cnmpt21  14981  ispsmet  15013  ismet  15034  isxmet  15035  metss  15184  qtopbasss  15211  cncfval  15262  elcncf2  15264  mulc1cncf  15279  cncfmet  15282  dedekindeulemloc  15309  dedekindeulemeu  15312  dedekindeu  15313  suplociccreex  15314  dedekindicclemloc  15318  dedekindicclemeu  15321  dedekindicclemicc  15322  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemloc  15331  ivthreinc  15335  dich0  15342  limccl  15349  ellimc3apf  15350  limcdifap  15352  limcmpted  15353  2irrexpqap  15668  perfectlem2  15690  2sqlem6  15815  2sqlem10  15820  wksfval  16068  wlkvtxedg  16109  clwwlkg  16136  bj-charfunbi  16257  bj-omtrans  16402  strcoll2  16429  strcollnfALT  16432  sscoll2  16434  2omap  16446  pw1nct  16456  0nninf  16458  nnsf  16459  peano4nninf  16460  nninfalllem1  16462  nninfself  16467  nninfsellemeq  16468  nninfsellemeqinf  16470  isomninnlem  16486  trilpolemlt1  16497  iswomninnlem  16505  iswomni0  16507  ismkvnnlem  16508  cndcap  16515  dceqnconst  16516  dcapnconst  16517  ltlenmkv  16526