Theorem ralbidv 2470

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  ralbii  2476  2ralbidv  2494  rexralbidv  2496  r19.32vdc  2619  raleqbi1dv  2673  raleqbidv  2677  cbvral2vw  2707  cbvral2v  2709  rspceaimv  2842  rspc2  2845  rspc3v  2850  reu6i  2921  reu7  2925  sbcralt  3031  sbcralg  3033  raaanlem  3520  2ralunsn  3785  elintg  3839  elintrabg  3844  eliin  3878  brralrspcev  4047  bnd2  4159  poeq1  4284  soeq1  4300  frforeq1  4328  frforeq3  4332  frirrg  4335  frind  4337  weeq1  4341  reusv3  4445  ontr2exmid  4509  reg2exmidlema  4518  posng  4683  ralxpf  4757  cnvpom  5153  funcnvuni  5267  fnmptfvd  5600  dff4im  5642  dff13f  5749  eusvobj2  5839  ovanraleqv  5877  ofreq  6064  smoeq  6269  recseq  6285  tfr0dm  6301  tfrlemiex  6310  tfr1onlemex  6326  tfr1onlemaccex  6327  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllemex  6339  tfrcllemaccex  6340  tfrcllemres  6341  elixp2  6680  xpf1o  6822  nneneq  6835  ac6sfi  6876  fimax2gtrilemstep  6878  fimax2gtri  6879  supeq1  6963  supeq3  6967  supmoti  6970  eqsupti  6973  supubti  6976  suplubti  6977  supisoex  6986  cnvinfex  6995  eqinfti  6997  infvalti  6999  updjud  7059  ctssdclemr  7089  nninff  7099  infnninf  7100  infnninfOLD  7101  nnnninf  7102  nnnninfeq  7104  nnnninfeq2  7105  enomnilem  7114  finomni  7116  exmidomni  7118  fodjuomnilemres  7124  ismkvnex  7131  fodjumkvlemres  7135  enmkvlem  7137  enwomnilem  7145  nninfdcinf  7147  nninfwlporlem  7149  nninfwlpoimlemg  7151  nninfwlpoimlemdc  7153  exmidontriimlem3  7200  exmidontriim  7202  cc2lem  7228  cc3  7230  elinp  7436  prloc  7453  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgpr  7644  caucvgprpr  7674  suplocexprlemloc  7683  suplocexpr  7687  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  caucvgsr  7764  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axcaucvglemcau  7860  axcaucvglemres  7861  axpre-suploclemres  7863  axpre-suploc  7864  lbreu  8861  sup3exmid  8873  nnsub  8917  indstr  9552  supinfneg  9554  infsupneg  9555  ublbneg  9572  lbzbi  9575  iccsupr  9923  frecuzrdgsuc  10370  frecuzrdgg  10372  frecuzrdgsuctlem  10379  seq3f1olemstep  10457  seq3f1olemp  10458  nn0ltexp2  10644  bccl  10701  cau4  11080  caubnd2  11081  maxleast  11177  rexanre  11184  rexico  11185  fimaxre2  11190  minmax  11193  xrminmax  11228  clim  11244  clim2  11246  clim2c  11247  clim0c  11249  climabs0  11270  cn1lem  11277  sumeq1  11318  prodeq1f  11515  zsupcllemstep  11900  infssuzex  11904  suprzubdc  11907  nninfdcex  11908  zsupssdc  11909  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlemex  11956  bezoutlemeu  11962  dfgcd3  11965  bezout  11966  dfgcd2  11969  nnwodc  11991  uzwodc  11992  nnwofdc  11993  sqrt2irr  12116  reumodprminv  12207  pc2dvds  12283  pcz  12285  prmpwdvds  12307  ennnfoneleminc  12366  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemnn0  12377  ennnfonelemr  12378  ennnfonelemim  12379  exmidunben  12381  ctinfomlemom  12382  ctinfom  12383  ctinf  12385  ctiunctlemudc  12392  ctiunct  12395  ssomct  12400  infpn2  12411  mgm1  12624  sgrp1  12651  mhmima  12706  dfgrp2  12732  isgrpinv  12756  grpidinv  12759  basgen2  12875  bastop1  12877  iscn  12991  cnpval  12992  iscnp  12993  iscnp3  12997  cnprcl2k  13000  lmbr  13007  lmbr2  13008  lmbrf  13009  cnptoprest  13033  cnptoprest2  13034  cnmpt21  13085  ispsmet  13117  ismet  13138  isxmet  13139  metss  13288  qtopbasss  13315  cncfval  13353  elcncf2  13355  mulc1cncf  13370  cncfmet  13373  dedekindeulemloc  13391  dedekindeulemeu  13394  dedekindeu  13395  suplociccreex  13396  dedekindicclemloc  13400  dedekindicclemeu  13403  dedekindicclemicc  13404  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemloc  13413  limccl  13422  ellimc3apf  13423  limcdifap  13425  limcmpted  13426  2irrexpqap  13690  2sqlem6  13750  2sqlem10  13755  bj-charfunbi  13846  bj-omtrans  13991  strcoll2  14018  strcollnfALT  14021  sscoll2  14023  pw1nct  14036  0nninf  14037  nnsf  14038  peano4nninf  14039  nninfalllem1  14041  nninfself  14046  nninfsellemeq  14047  nninfsellemeqinf  14049  isomninnlem  14062  trilpolemlt1  14073  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084  dceqnconst  14091  dcapnconst  14092