Theorem ralbidv 2550

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralbii  2556  2ralbidv  2574  rexralbidv  2576  r19.32vdc  2700  raleqbi1dv  2761  raleqbidv  2765  cbvral2vw  2797  cbvral2v  2799  rspceaimv  2938  rspc2  2941  rspc3v  2946  reu6i  3017  reu7  3021  sbcralt  3128  sbcralg  3130  reu8nf  3133  raaanlem  3632  2ralunsn  3924  elintg  3978  elintrabg  3983  eliin  4017  brralrspcev  4190  bnd2  4312  poeq1  4446  soeq1  4462  frforeq1  4490  frforeq3  4494  frirrg  4497  frind  4499  weeq1  4503  reusv3  4608  ontr2exmid  4674  reg2exmidlema  4683  posng  4849  ralxpf  4928  cnvpom  5333  funcnvuni  5453  fnmptfvd  5816  dff4im  5857  dff13f  5979  eusvobj2  6074  ovanraleqv  6112  ofreq  6309  caofdig  6340  uchoice  6375  suppssrst  6505  suppssrgst  6506  suppofss1dcl  6508  suppofss2dcl  6509  smoeq  6565  recseq  6581  tfr0dm  6597  tfrlemiex  6606  tfr1onlemex  6622  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemex  6635  tfrcllemaccex  6636  tfrcllemres  6637  elixp2  6988  pw2f1odclem  7138  xpf1o  7148  nneneq  7162  ac6sfi  7206  fimax2gtrilemstep  7209  fimax2gtri  7210  elssdc  7213  opabfi  7251  2omap  7324  supeq1  7332  supeq3  7336  supmoti  7339  eqsupti  7342  supubti  7345  suplubti  7346  supisoex  7355  cnvinfex  7364  eqinfti  7366  infvalti  7368  updjud  7428  ctssdclemr  7458  nninff  7468  nninfninc  7469  infnninf  7470  infnninfOLD  7471  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  enomnilem  7484  finomni  7486  exmidomni  7488  fodjuomnilemres  7494  ismkvnex  7501  fodjumkvlemres  7505  enmkvlem  7507  enwomnilem  7515  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemg  7521  nninfwlpoimlemdc  7523  exmidontriimlem3  7585  exmidontriim  7587  papeq1  7615  papsym  7618  papcotr  7619  tapeq1  7624  netap  7626  exmidapne  7632  cc2lem  7638  cc3  7640  elinp  7847  prloc  7864  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgpr  8055  caucvgprpr  8085  suplocexprlemloc  8094  suplocexpr  8098  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  caucvgsr  8175  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  lbreu  9283  sup3exmid  9295  nnsub  9352  indstr  10009  supinfneg  10011  infsupneg  10012  ublbneg  10029  lbzbi  10032  iccsupr  10385  zsupcllemstep  10679  infssuzex  10683  suprzubdc  10688  nninfdcex  10689  zsupssdc  10690  frecuzrdgsuc  10872  frecuzrdgg  10874  frecuzrdgsuctlem  10881  seq3f1olemstep  10972  seq3f1olemp  10973  seqfeq4g  10989  nn0ltexp2  11169  bccl  11227  hashfibc  11305  wrdind  11516  wrd2ind  11517  cau4  11905  caubnd2  11906  maxleast  12002  rexanre  12009  rexico  12010  fimaxre2  12016  fiidxsupcl  12018  minmax  12020  xrminmax  12056  clim  12072  clim2  12074  clim2c  12075  clim0c  12077  climabs0  12098  cn1lem  12105  sumeq1  12146  prodeq1f  12344  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemeu  12809  dfgcd3  12812  bezout  12813  dfgcd2  12816  nnwodc  12838  uzwodc  12839  nnwofdc  12840  sqrt2irr  12966  reumodprminv  13061  pc2dvds  13138  pcz  13140  prmpwdvds  13163  ballotfileme  13294  ennnfoneleminc  13360  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemnn0  13371  ennnfonelemr  13372  ennnfonelemim  13373  exmidunben  13375  ctinfomlemom  13376  ctinfom  13377  ctinf  13379  ctiunctlemudc  13386  ctiunct  13389  ssomct  13394  infpn2  13405  imasaddfnlemg  13694  mgm1  13749  sgrp1  13785  mhmima  13857  dfgrp2  13891  isgrpinv  13918  grpidinv  13923  dfgrp3mlem  13962  issubg4m  14055  isnsg2  14065  elnmz  14070  ghmrn  14119  ghmnsgima  14130  cntzex  14150  cntzfval  14152  elcntz  14154  resscntz  14166  srgideu  14383  ring1  14471  lringuplu  14612  subrgugrp  14657  isrrg  14680  islssm  14803  islssmg  14804  rnglidlmcl  14926  isassa  15111  mplsubgfilemm  15214  mplsubgfilemcl  15215  basgen2  15307  bastop1  15309  iscn  15423  cnpval  15424  iscnp  15425  iscnp3  15429  cnprcl2k  15432  lmbr  15439  lmbr2  15440  lmbrf  15441  cnptoprest  15465  cnptoprest2  15466  cnmpt21  15517  ispsmet  15549  ismet  15570  isxmet  15571  metss  15720  qtopbasss  15747  cncfval  15798  elcncf2  15800  mulc1cncf  15815  cncfmet  15818  dedekindeulemloc  15845  dedekindeulemeu  15848  dedekindeu  15849  suplociccreex  15850  dedekindicclemloc  15854  dedekindicclemeu  15857  dedekindicclemicc  15858  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemloc  15867  ivthreinc  15871  dich0  15878  limccl  15885  ellimc3apf  15886  limcdifap  15888  limcmpted  15889  2irrexpqap  16214  zprmlogbaplem2  16216  zprmlogbap  16218  perfectlem2  16300  prmefexple  16308  bposlem1  16311  2sqlem6  16444  2sqlem10  16449  wksfval  16768  wlkvtxedg  16809  clwwlkg  16839  depind  16955  bj-charfunbi  17042  bj-omtrans  17187  strcoll2  17214  strcollnfALT  17217  sscoll2  17219  pw1nct  17238  exmidcon  17242  0nninf  17253  nnsf  17254  peano4nninf  17255  nninfalllem1  17257  nninfself  17262  nninfsellemeq  17263  nninfsellemeqinf  17265  isomninnlem  17285  rirrdisj  17291  trilpolemlt1  17297  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309  cndcap  17316  dceqnconst  17317  dcapnconst  17318  ltlenmkv  17327