Theorem ralbidv 2497

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralbii  2503  2ralbidv  2521  rexralbidv  2523  r19.32vdc  2646  raleqbi1dv  2705  raleqbidv  2709  cbvral2vw  2740  cbvral2v  2742  rspceaimv  2876  rspc2  2879  rspc3v  2884  reu6i  2955  reu7  2959  sbcralt  3066  sbcralg  3068  raaanlem  3556  2ralunsn  3829  elintg  3883  elintrabg  3888  eliin  3922  brralrspcev  4092  bnd2  4207  poeq1  4335  soeq1  4351  frforeq1  4379  frforeq3  4383  frirrg  4386  frind  4388  weeq1  4392  reusv3  4496  ontr2exmid  4562  reg2exmidlema  4571  posng  4736  ralxpf  4813  cnvpom  5213  funcnvuni  5328  fnmptfvd  5669  dff4im  5711  dff13f  5820  eusvobj2  5911  ovanraleqv  5949  ofreq  6143  caofdig  6173  uchoice  6204  smoeq  6357  recseq  6373  tfr0dm  6389  tfrlemiex  6398  tfr1onlemex  6414  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemex  6427  tfrcllemaccex  6428  tfrcllemres  6429  elixp2  6770  pw2f1odclem  6904  xpf1o  6914  nneneq  6927  ac6sfi  6968  fimax2gtrilemstep  6970  fimax2gtri  6971  opabfi  7008  supeq1  7061  supeq3  7065  supmoti  7068  eqsupti  7071  supubti  7074  suplubti  7075  supisoex  7084  cnvinfex  7093  eqinfti  7095  infvalti  7097  updjud  7157  ctssdclemr  7187  nninff  7197  nninfninc  7198  infnninf  7199  infnninfOLD  7200  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  finomni  7215  exmidomni  7217  fodjuomnilemres  7223  ismkvnex  7230  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemg  7250  nninfwlpoimlemdc  7252  exmidontriimlem3  7308  exmidontriim  7310  tapeq1  7337  netap  7339  exmidapne  7345  cc2lem  7351  cc3  7353  elinp  7560  prloc  7577  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgpr  7768  caucvgprpr  7798  suplocexprlemloc  7807  suplocexpr  7811  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  caucvgsr  7888  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  axcaucvglemcau  7984  axcaucvglemres  7985  axpre-suploclemres  7987  axpre-suploc  7988  lbreu  8991  sup3exmid  9003  nnsub  9048  indstr  9686  supinfneg  9688  infsupneg  9689  ublbneg  9706  lbzbi  9709  iccsupr  10060  zsupcllemstep  10338  infssuzex  10342  suprzubdc  10345  nninfdcex  10346  zsupssdc  10347  frecuzrdgsuc  10525  frecuzrdgg  10527  frecuzrdgsuctlem  10534  seq3f1olemstep  10625  seq3f1olemp  10626  seqfeq4g  10642  nn0ltexp2  10820  bccl  10878  cau4  11300  caubnd2  11301  maxleast  11397  rexanre  11404  rexico  11405  fimaxre2  11411  minmax  11414  xrminmax  11449  clim  11465  clim2  11467  clim2c  11468  clim0c  11470  climabs0  11491  cn1lem  11498  sumeq1  11539  prodeq1f  11736  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemex  12195  bezoutlemeu  12201  dfgcd3  12204  bezout  12205  dfgcd2  12208  nnwodc  12230  uzwodc  12231  nnwofdc  12232  sqrt2irr  12357  reumodprminv  12449  pc2dvds  12526  pcz  12528  prmpwdvds  12551  ennnfoneleminc  12655  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemnn0  12666  ennnfonelemr  12667  ennnfonelemim  12668  exmidunben  12670  ctinfomlemom  12671  ctinfom  12672  ctinf  12674  ctiunctlemudc  12681  ctiunct  12684  ssomct  12689  infpn2  12700  imasaddfnlemg  13018  mgm1  13074  sgrp1  13115  mhmima  13195  dfgrp2  13231  isgrpinv  13258  grpidinv  13263  dfgrp3mlem  13302  issubg4m  13401  isnsg2  13411  elnmz  13416  ghmrn  13465  ghmnsgima  13476  srgideu  13606  ring1  13693  lringuplu  13830  subrgugrp  13874  isrrg  13897  islssm  13991  islssmg  13992  rnglidlmcl  14114  mplsubgfilemm  14332  mplsubgfilemcl  14333  basgen2  14425  bastop1  14427  iscn  14541  cnpval  14542  iscnp  14543  iscnp3  14547  cnprcl2k  14550  lmbr  14557  lmbr2  14558  lmbrf  14559  cnptoprest  14583  cnptoprest2  14584  cnmpt21  14635  ispsmet  14667  ismet  14688  isxmet  14689  metss  14838  qtopbasss  14865  cncfval  14916  elcncf2  14918  mulc1cncf  14933  cncfmet  14936  dedekindeulemloc  14963  dedekindeulemeu  14966  dedekindeu  14967  suplociccreex  14968  dedekindicclemloc  14972  dedekindicclemeu  14975  dedekindicclemicc  14976  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemloc  14985  ivthreinc  14989  dich0  14996  limccl  15003  ellimc3apf  15004  limcdifap  15006  limcmpted  15007  2irrexpqap  15322  perfectlem2  15344  2sqlem6  15469  2sqlem10  15474  bj-charfunbi  15565  bj-omtrans  15710  strcoll2  15737  strcollnfALT  15740  sscoll2  15742  2omap  15750  pw1nct  15758  0nninf  15759  nnsf  15760  peano4nninf  15761  nninfalllem1  15763  nninfself  15768  nninfsellemeq  15769  nninfsellemeqinf  15771  isomninnlem  15787  trilpolemlt1  15798  iswomninnlem  15806  iswomni0  15808  ismkvnnlem  15809  cndcap  15816  dceqnconst  15817  dcapnconst  15818  ltlenmkv  15827