Theorem ralbidv 2438

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

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

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  ralbii  2444  2ralbidv  2462  rexralbidv  2464  r19.32vdc  2583  raleqbi1dv  2637  raleqbidv  2641  cbvral2v  2668  rspceaimv  2801  rspc2  2804  rspc3v  2809  reu6i  2879  reu7  2883  sbcralt  2989  sbcralg  2991  raaanlem  3473  2ralunsn  3733  elintg  3787  elintrabg  3792  eliin  3826  brralrspcev  3994  bnd2  4105  poeq1  4229  soeq1  4245  frforeq1  4273  frforeq3  4277  frirrg  4280  frind  4282  weeq1  4286  reusv3  4389  ontr2exmid  4448  reg2exmidlema  4457  posng  4619  ralxpf  4693  cnvpom  5089  funcnvuni  5200  dff4im  5574  dff13f  5679  eusvobj2  5768  ovanraleqv  5806  ofreq  5993  smoeq  6195  recseq  6211  tfr0dm  6227  tfrlemiex  6236  tfr1onlemex  6252  tfr1onlemaccex  6253  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllemex  6265  tfrcllemaccex  6266  tfrcllemres  6267  elixp2  6604  xpf1o  6746  nneneq  6759  ac6sfi  6800  fimax2gtrilemstep  6802  fimax2gtri  6803  supeq1  6881  supeq3  6885  supmoti  6888  eqsupti  6891  supubti  6894  suplubti  6895  supisoex  6904  cnvinfex  6913  eqinfti  6915  infvalti  6917  updjud  6975  ctssdclemr  7005  enomnilem  7018  finomni  7020  exmidomni  7022  fodjuomnilemres  7028  infnninf  7030  nnnninf  7031  ismkvnex  7037  fodjumkvlemres  7041  enmkvlem  7043  enwomnilem  7050  cc2lem  7098  cc3  7100  elinp  7306  prloc  7323  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgpr  7514  caucvgprpr  7544  suplocexprlemloc  7553  suplocexpr  7557  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  caucvgsr  7634  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  axcaucvglemcau  7730  axcaucvglemres  7731  axpre-suploclemres  7733  axpre-suploc  7734  lbreu  8727  sup3exmid  8739  nnsub  8783  indstr  9415  supinfneg  9417  infsupneg  9418  ublbneg  9432  lbzbi  9435  iccsupr  9779  frecuzrdgsuc  10218  frecuzrdgg  10220  frecuzrdgsuctlem  10227  seq3f1olemstep  10305  seq3f1olemp  10306  bccl  10545  cau4  10920  caubnd2  10921  maxleast  11017  rexanre  11024  rexico  11025  fimaxre2  11030  minmax  11033  xrminmax  11066  clim  11082  clim2  11084  clim2c  11085  clim0c  11087  climabs0  11108  cn1lem  11115  sumeq1  11156  prodeq1f  11353  zsupcllemstep  11674  infssuzex  11678  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemeu  11731  dfgcd3  11734  bezout  11735  dfgcd2  11738  sqrt2irr  11876  ennnfoneleminc  11960  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemnn0  11971  ennnfonelemr  11972  ennnfonelemim  11973  exmidunben  11975  ctinfomlemom  11976  ctinfom  11977  ctinf  11979  ctiunctlemudc  11986  ctiunct  11989  basgen2  12289  bastop1  12291  iscn  12405  cnpval  12406  iscnp  12407  iscnp3  12411  cnprcl2k  12414  lmbr  12421  lmbr2  12422  lmbrf  12423  cnptoprest  12447  cnptoprest2  12448  cnmpt21  12499  ispsmet  12531  ismet  12552  isxmet  12553  metss  12702  qtopbasss  12729  cncfval  12767  elcncf2  12769  mulc1cncf  12784  cncfmet  12787  dedekindeulemloc  12805  dedekindeulemeu  12808  dedekindeu  12809  suplociccreex  12810  dedekindicclemloc  12814  dedekindicclemeu  12817  dedekindicclemicc  12818  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemloc  12827  limccl  12836  ellimc3apf  12837  limcdifap  12839  limcmpted  12840  2irrexpqap  13103  bj-omtrans  13325  strcoll2  13352  strcollnfALT  13355  sscoll2  13357  pw1nct  13371  0nninf  13372  nninff  13373  nnsf  13374  peano4nninf  13375  nninfalllemn  13377  nninfalllem1  13378  nninfself  13384  nninfsellemeq  13385  nninfsellemeqinf  13387  isomninnlem  13400  trilpolemlt1  13409  iswomninnlem  13417  ismkvnnlem  13419  dceqnconst  13423