Theorem ralbidv 2457

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 2455	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

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

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440

This theorem is referenced by:  ralbii  2463  2ralbidv  2481  rexralbidv  2483  r19.32vdc  2606  raleqbi1dv  2660  raleqbidv  2664  cbvral2v  2691  rspceaimv  2824  rspc2  2827  rspc3v  2832  reu6i  2903  reu7  2907  sbcralt  3013  sbcralg  3015  raaanlem  3499  2ralunsn  3762  elintg  3816  elintrabg  3821  eliin  3855  brralrspcev  4023  bnd2  4135  poeq1  4260  soeq1  4276  frforeq1  4304  frforeq3  4308  frirrg  4311  frind  4313  weeq1  4317  reusv3  4421  ontr2exmid  4485  reg2exmidlema  4494  posng  4659  ralxpf  4733  cnvpom  5129  funcnvuni  5240  dff4im  5614  dff13f  5721  eusvobj2  5811  ovanraleqv  5849  ofreq  6036  smoeq  6238  recseq  6254  tfr0dm  6270  tfrlemiex  6279  tfr1onlemex  6295  tfr1onlemaccex  6296  tfrcllemsucaccv  6302  tfrcllembxssdm  6304  tfrcllemex  6308  tfrcllemaccex  6309  tfrcllemres  6310  elixp2  6648  xpf1o  6790  nneneq  6803  ac6sfi  6844  fimax2gtrilemstep  6846  fimax2gtri  6847  supeq1  6931  supeq3  6935  supmoti  6938  eqsupti  6941  supubti  6944  suplubti  6945  supisoex  6954  cnvinfex  6963  eqinfti  6965  infvalti  6967  updjud  7027  ctssdclemr  7057  nninff  7067  infnninf  7068  infnninfOLD  7069  nnnninf  7070  nnnninfeq  7072  nnnninfeq2  7073  enomnilem  7082  finomni  7084  exmidomni  7086  fodjuomnilemres  7092  ismkvnex  7099  fodjumkvlemres  7103  enmkvlem  7105  enwomnilem  7113  exmidontriimlem3  7159  exmidontriim  7161  cc2lem  7187  cc3  7189  elinp  7395  prloc  7412  cauappcvgprlemladdru  7577  cauappcvgprlemladdrl  7578  caucvgpr  7603  caucvgprpr  7633  suplocexprlemloc  7642  suplocexpr  7646  caucvgsrlemgt1  7716  caucvgsrlemoffres  7721  caucvgsr  7723  suplocsrlemb  7727  suplocsrlempr  7728  suplocsrlem  7729  axcaucvglemcau  7819  axcaucvglemres  7820  axpre-suploclemres  7822  axpre-suploc  7823  lbreu  8817  sup3exmid  8829  nnsub  8873  indstr  9505  supinfneg  9507  infsupneg  9508  ublbneg  9523  lbzbi  9526  iccsupr  9871  frecuzrdgsuc  10317  frecuzrdgg  10319  frecuzrdgsuctlem  10326  seq3f1olemstep  10404  seq3f1olemp  10405  bccl  10645  cau4  11020  caubnd2  11021  maxleast  11117  rexanre  11124  rexico  11125  fimaxre2  11130  minmax  11133  xrminmax  11166  clim  11182  clim2  11184  clim2c  11185  clim0c  11187  climabs0  11208  cn1lem  11215  sumeq1  11256  prodeq1f  11453  zsupcllemstep  11836  infssuzex  11840  nninfdcex  11843  bezoutlemstep  11885  bezoutlemmain  11886  bezoutlemex  11889  bezoutlemeu  11895  dfgcd3  11898  bezout  11899  dfgcd2  11902  sqrt2irr  12041  reumodprminv  12132  ennnfoneleminc  12182  ennnfonelemex  12185  ennnfonelemhom  12186  ennnfonelemnn0  12193  ennnfonelemr  12194  ennnfonelemim  12195  exmidunben  12197  ctinfomlemom  12198  ctinfom  12199  ctinf  12201  ctiunctlemudc  12208  ctiunct  12211  ssomct  12216  basgen2  12523  bastop1  12525  iscn  12639  cnpval  12640  iscnp  12641  iscnp3  12645  cnprcl2k  12648  lmbr  12655  lmbr2  12656  lmbrf  12657  cnptoprest  12681  cnptoprest2  12682  cnmpt21  12733  ispsmet  12765  ismet  12786  isxmet  12787  metss  12936  qtopbasss  12963  cncfval  13001  elcncf2  13003  mulc1cncf  13018  cncfmet  13021  dedekindeulemloc  13039  dedekindeulemeu  13042  dedekindeu  13043  suplociccreex  13044  dedekindicclemloc  13048  dedekindicclemeu  13051  dedekindicclemicc  13052  ivthinclemlopn  13056  ivthinclemlr  13057  ivthinclemuopn  13058  ivthinclemur  13059  ivthinclemloc  13061  limccl  13070  ellimc3apf  13071  limcdifap  13073  limcmpted  13074  2irrexpqap  13337  bj-charfunbi  13428  bj-omtrans  13573  strcoll2  13600  strcollnfALT  13603  sscoll2  13605  pw1nct  13617  0nninf  13618  nnsf  13619  peano4nninf  13620  nninfalllem1  13622  nninfself  13627  nninfsellemeq  13628  nninfsellemeqinf  13630  isomninnlem  13643  trilpolemlt1  13654  iswomninnlem  13662  iswomni0  13664  ismkvnnlem  13665  dceqnconst  13672  dcapnconst  13673