Theorem ralbidv 2465

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

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

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2448

This theorem is referenced by:  ralbii  2471  2ralbidv  2489  rexralbidv  2491  r19.32vdc  2614  raleqbi1dv  2668  raleqbidv  2672  cbvral2vw  2702  cbvral2v  2704  rspceaimv  2837  rspc2  2840  rspc3v  2845  reu6i  2916  reu7  2920  sbcralt  3026  sbcralg  3028  raaanlem  3513  2ralunsn  3777  elintg  3831  elintrabg  3836  eliin  3870  brralrspcev  4039  bnd2  4151  poeq1  4276  soeq1  4292  frforeq1  4320  frforeq3  4324  frirrg  4327  frind  4329  weeq1  4333  reusv3  4437  ontr2exmid  4501  reg2exmidlema  4510  posng  4675  ralxpf  4749  cnvpom  5145  funcnvuni  5256  dff4im  5630  dff13f  5737  eusvobj2  5827  ovanraleqv  5865  ofreq  6052  smoeq  6254  recseq  6270  tfr0dm  6286  tfrlemiex  6295  tfr1onlemex  6311  tfr1onlemaccex  6312  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllemex  6324  tfrcllemaccex  6325  tfrcllemres  6326  elixp2  6664  xpf1o  6806  nneneq  6819  ac6sfi  6860  fimax2gtrilemstep  6862  fimax2gtri  6863  supeq1  6947  supeq3  6951  supmoti  6954  eqsupti  6957  supubti  6960  suplubti  6961  supisoex  6970  cnvinfex  6979  eqinfti  6981  infvalti  6983  updjud  7043  ctssdclemr  7073  nninff  7083  infnninf  7084  infnninfOLD  7085  nnnninf  7086  nnnninfeq  7088  nnnninfeq2  7089  enomnilem  7098  finomni  7100  exmidomni  7102  fodjuomnilemres  7108  ismkvnex  7115  fodjumkvlemres  7119  enmkvlem  7121  enwomnilem  7129  exmidontriimlem3  7175  exmidontriim  7177  cc2lem  7203  cc3  7205  elinp  7411  prloc  7428  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  caucvgpr  7619  caucvgprpr  7649  suplocexprlemloc  7658  suplocexpr  7662  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  caucvgsr  7739  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  axcaucvglemcau  7835  axcaucvglemres  7836  axpre-suploclemres  7838  axpre-suploc  7839  lbreu  8836  sup3exmid  8848  nnsub  8892  indstr  9527  supinfneg  9529  infsupneg  9530  ublbneg  9547  lbzbi  9550  iccsupr  9898  frecuzrdgsuc  10345  frecuzrdgg  10347  frecuzrdgsuctlem  10354  seq3f1olemstep  10432  seq3f1olemp  10433  nn0ltexp2  10619  bccl  10676  cau4  11054  caubnd2  11055  maxleast  11151  rexanre  11158  rexico  11159  fimaxre2  11164  minmax  11167  xrminmax  11202  clim  11218  clim2  11220  clim2c  11221  clim0c  11223  climabs0  11244  cn1lem  11251  sumeq1  11292  prodeq1f  11489  zsupcllemstep  11874  infssuzex  11878  suprzubdc  11881  nninfdcex  11882  zsupssdc  11883  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlemex  11930  bezoutlemeu  11936  dfgcd3  11939  bezout  11940  dfgcd2  11943  nnwodc  11965  uzwodc  11966  nnwofdc  11967  sqrt2irr  12090  reumodprminv  12181  pc2dvds  12257  pcz  12259  prmpwdvds  12281  ennnfoneleminc  12340  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemnn0  12351  ennnfonelemr  12352  ennnfonelemim  12353  exmidunben  12355  ctinfomlemom  12356  ctinfom  12357  ctinf  12359  ctiunctlemudc  12366  ctiunct  12369  ssomct  12374  infpn2  12385  basgen2  12681  bastop1  12683  iscn  12797  cnpval  12798  iscnp  12799  iscnp3  12803  cnprcl2k  12806  lmbr  12813  lmbr2  12814  lmbrf  12815  cnptoprest  12839  cnptoprest2  12840  cnmpt21  12891  ispsmet  12923  ismet  12944  isxmet  12945  metss  13094  qtopbasss  13121  cncfval  13159  elcncf2  13161  mulc1cncf  13176  cncfmet  13179  dedekindeulemloc  13197  dedekindeulemeu  13200  dedekindeu  13201  suplociccreex  13202  dedekindicclemloc  13206  dedekindicclemeu  13209  dedekindicclemicc  13210  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemloc  13219  limccl  13228  ellimc3apf  13229  limcdifap  13231  limcmpted  13232  2irrexpqap  13496  2sqlem6  13556  2sqlem10  13561  bj-charfunbi  13653  bj-omtrans  13798  strcoll2  13825  strcollnfALT  13828  sscoll2  13830  pw1nct  13843  0nninf  13844  nnsf  13845  peano4nninf  13846  nninfalllem1  13848  nninfself  13853  nninfsellemeq  13854  nninfsellemeqinf  13856  isomninnlem  13869  trilpolemlt1  13880  iswomninnlem  13888  iswomni0  13890  ismkvnnlem  13891  dceqnconst  13898  dcapnconst  13899