Theorem ralbidv 2497

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralbii  2503  2ralbidv  2521  rexralbidv  2523  r19.32vdc  2646  raleqbi1dv  2705  raleqbidv  2709  cbvral2vw  2740  cbvral2v  2742  rspceaimv  2876  rspc2  2879  rspc3v  2884  reu6i  2955  reu7  2959  sbcralt  3066  sbcralg  3068  raaanlem  3555  2ralunsn  3828  elintg  3882  elintrabg  3887  eliin  3921  brralrspcev  4091  bnd2  4206  poeq1  4334  soeq1  4350  frforeq1  4378  frforeq3  4382  frirrg  4385  frind  4387  weeq1  4391  reusv3  4495  ontr2exmid  4561  reg2exmidlema  4570  posng  4735  ralxpf  4812  cnvpom  5212  funcnvuni  5327  fnmptfvd  5666  dff4im  5708  dff13f  5817  eusvobj2  5908  ovanraleqv  5946  ofreq  6139  caofdig  6164  uchoice  6195  smoeq  6348  recseq  6364  tfr0dm  6380  tfrlemiex  6389  tfr1onlemex  6405  tfr1onlemaccex  6406  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllemex  6418  tfrcllemaccex  6419  tfrcllemres  6420  elixp2  6761  pw2f1odclem  6895  xpf1o  6905  nneneq  6918  ac6sfi  6959  fimax2gtrilemstep  6961  fimax2gtri  6962  opabfi  6999  supeq1  7052  supeq3  7056  supmoti  7059  eqsupti  7062  supubti  7065  suplubti  7066  supisoex  7075  cnvinfex  7084  eqinfti  7086  infvalti  7088  updjud  7148  ctssdclemr  7178  nninff  7188  nninfninc  7189  infnninf  7190  infnninfOLD  7191  nnnninf  7192  nnnninfeq  7194  nnnninfeq2  7195  enomnilem  7204  finomni  7206  exmidomni  7208  fodjuomnilemres  7214  ismkvnex  7221  fodjumkvlemres  7225  enmkvlem  7227  enwomnilem  7235  nninfdcinf  7237  nninfwlporlem  7239  nninfwlpoimlemg  7241  nninfwlpoimlemdc  7243  exmidontriimlem3  7290  exmidontriim  7292  tapeq1  7319  netap  7321  exmidapne  7327  cc2lem  7333  cc3  7335  elinp  7541  prloc  7558  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgpr  7749  caucvgprpr  7779  suplocexprlemloc  7788  suplocexpr  7792  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  caucvgsr  7869  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  axcaucvglemcau  7965  axcaucvglemres  7966  axpre-suploclemres  7968  axpre-suploc  7969  lbreu  8972  sup3exmid  8984  nnsub  9029  indstr  9667  supinfneg  9669  infsupneg  9670  ublbneg  9687  lbzbi  9690  iccsupr  10041  zsupcllemstep  10319  infssuzex  10323  suprzubdc  10326  nninfdcex  10327  zsupssdc  10328  frecuzrdgsuc  10506  frecuzrdgg  10508  frecuzrdgsuctlem  10515  seq3f1olemstep  10606  seq3f1olemp  10607  seqfeq4g  10623  nn0ltexp2  10801  bccl  10859  cau4  11281  caubnd2  11282  maxleast  11378  rexanre  11385  rexico  11386  fimaxre2  11392  minmax  11395  xrminmax  11430  clim  11446  clim2  11448  clim2c  11449  clim0c  11451  climabs0  11472  cn1lem  11479  sumeq1  11520  prodeq1f  11717  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlemex  12168  bezoutlemeu  12174  dfgcd3  12177  bezout  12178  dfgcd2  12181  nnwodc  12203  uzwodc  12204  nnwofdc  12205  sqrt2irr  12330  reumodprminv  12422  pc2dvds  12499  pcz  12501  prmpwdvds  12524  ennnfoneleminc  12628  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemnn0  12639  ennnfonelemr  12640  ennnfonelemim  12641  exmidunben  12643  ctinfomlemom  12644  ctinfom  12645  ctinf  12647  ctiunctlemudc  12654  ctiunct  12657  ssomct  12662  infpn2  12673  imasaddfnlemg  12957  mgm1  13013  sgrp1  13054  mhmima  13123  dfgrp2  13159  isgrpinv  13186  grpidinv  13191  dfgrp3mlem  13230  issubg4m  13323  isnsg2  13333  elnmz  13338  ghmrn  13387  ghmnsgima  13398  srgideu  13528  ring1  13615  lringuplu  13752  subrgugrp  13796  isrrg  13819  islssm  13913  islssmg  13914  rnglidlmcl  14036  basgen2  14317  bastop1  14319  iscn  14433  cnpval  14434  iscnp  14435  iscnp3  14439  cnprcl2k  14442  lmbr  14449  lmbr2  14450  lmbrf  14451  cnptoprest  14475  cnptoprest2  14476  cnmpt21  14527  ispsmet  14559  ismet  14580  isxmet  14581  metss  14730  qtopbasss  14757  cncfval  14808  elcncf2  14810  mulc1cncf  14825  cncfmet  14828  dedekindeulemloc  14855  dedekindeulemeu  14858  dedekindeu  14859  suplociccreex  14860  dedekindicclemloc  14864  dedekindicclemeu  14867  dedekindicclemicc  14868  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemloc  14877  ivthreinc  14881  dich0  14888  limccl  14895  ellimc3apf  14896  limcdifap  14898  limcmpted  14899  2irrexpqap  15214  perfectlem2  15236  2sqlem6  15361  2sqlem10  15366  bj-charfunbi  15457  bj-omtrans  15602  strcoll2  15629  strcollnfALT  15632  sscoll2  15634  pw1nct  15647  0nninf  15648  nnsf  15649  peano4nninf  15650  nninfalllem1  15652  nninfself  15657  nninfsellemeq  15658  nninfsellemeqinf  15660  isomninnlem  15674  trilpolemlt1  15685  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696  cndcap  15703  dceqnconst  15704  dcapnconst  15705  ltlenmkv  15714