Theorem ralbidv 2437

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

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

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  ralbii  2441  2ralbidv  2459  rexralbidv  2461  r19.32vdc  2580  raleqbi1dv  2634  raleqbidv  2638  cbvral2v  2665  rspceaimv  2797  rspc2  2800  rspc3v  2805  reu6i  2875  reu7  2879  sbcralt  2985  sbcralg  2987  raaanlem  3468  2ralunsn  3725  elintg  3779  elintrabg  3784  eliin  3818  brralrspcev  3986  bnd2  4097  poeq1  4221  soeq1  4237  frforeq1  4265  frforeq3  4269  frirrg  4272  frind  4274  weeq1  4278  reusv3  4381  ontr2exmid  4440  reg2exmidlema  4449  posng  4611  ralxpf  4685  cnvpom  5081  funcnvuni  5192  dff4im  5566  dff13f  5671  eusvobj2  5760  ovanraleqv  5798  ofreq  5985  smoeq  6187  recseq  6203  tfr0dm  6219  tfrlemiex  6228  tfr1onlemex  6244  tfr1onlemaccex  6245  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllemex  6257  tfrcllemaccex  6258  tfrcllemres  6259  elixp2  6596  xpf1o  6738  nneneq  6751  ac6sfi  6792  fimax2gtrilemstep  6794  fimax2gtri  6795  supeq1  6873  supeq3  6877  supmoti  6880  eqsupti  6883  supubti  6886  suplubti  6887  supisoex  6896  cnvinfex  6905  eqinfti  6907  infvalti  6909  updjud  6967  ctssdclemr  6997  enomnilem  7010  finomni  7012  exmidomni  7014  fodjuomnilemres  7020  infnninf  7022  nnnninf  7023  ismkvnex  7029  fodjumkvlemres  7033  elinp  7282  prloc  7299  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgpr  7490  caucvgprpr  7520  suplocexprlemloc  7529  suplocexpr  7533  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  caucvgsr  7610  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  axcaucvglemcau  7706  axcaucvglemres  7707  axpre-suploclemres  7709  axpre-suploc  7710  lbreu  8703  sup3exmid  8715  nnsub  8759  indstr  9388  supinfneg  9390  infsupneg  9391  ublbneg  9405  lbzbi  9408  iccsupr  9749  frecuzrdgsuc  10187  frecuzrdgg  10189  frecuzrdgsuctlem  10196  seq3f1olemstep  10274  seq3f1olemp  10275  bccl  10513  cau4  10888  caubnd2  10889  maxleast  10985  rexanre  10992  rexico  10993  fimaxre2  10998  minmax  11001  xrminmax  11034  clim  11050  clim2  11052  clim2c  11053  clim0c  11055  climabs0  11076  cn1lem  11083  sumeq1  11124  prodeq1f  11321  zsupcllemstep  11638  infssuzex  11642  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlemex  11689  bezoutlemeu  11695  dfgcd3  11698  bezout  11699  dfgcd2  11702  sqrt2irr  11840  ennnfoneleminc  11924  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemnn0  11935  ennnfonelemr  11936  ennnfonelemim  11937  exmidunben  11939  ctinfomlemom  11940  ctinfom  11941  ctinf  11943  ctiunctlemudc  11950  ctiunct  11953  basgen2  12250  bastop1  12252  iscn  12366  cnpval  12367  iscnp  12368  iscnp3  12372  cnprcl2k  12375  lmbr  12382  lmbr2  12383  lmbrf  12384  cnptoprest  12408  cnptoprest2  12409  cnmpt21  12460  ispsmet  12492  ismet  12513  isxmet  12514  metss  12663  qtopbasss  12690  cncfval  12728  elcncf2  12730  mulc1cncf  12745  cncfmet  12748  dedekindeulemloc  12766  dedekindeulemeu  12769  dedekindeu  12770  suplociccreex  12771  dedekindicclemloc  12775  dedekindicclemeu  12778  dedekindicclemicc  12779  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemloc  12788  limccl  12797  ellimc3apf  12798  limcdifap  12800  limcmpted  12801  bj-omtrans  13154  0nninf  13197  nninff  13198  nnsf  13199  peano4nninf  13200  nninfalllemn  13202  nninfalllem1  13203  nninfself  13209  nninfsellemeq  13210  nninfsellemeqinf  13212  isomninnlem  13225  trilpolemlt1  13234