Theorem ralbidva 3187

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 29-Dec-2019.)

Hypothesis

Ref	Expression
ralbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ralbidva	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidva

Step	Hyp	Ref	Expression
1		ralbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.74da 816	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜒)))
3	2	ralbidv2 3185	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081

This theorem is used by:  ralbidv  3189  2ralbidva  3228  raleqbidva  3329  poinxp  5737  soinxp  5738  frinxp  5739  ordunisssuc  6486  fnmptfvd  7060  funimass3  7073  fnnfpeq0  7203  cocan1  7319  cocan2  7320  isores2  7361  isoini2  7367  ofrfvalg  7722  ofrfval2  7735  caofidlcan  7752  tfindsg2  7894  f1oweALT  8005  fnwe2lem3  8171  fnsuppres  8233  dfsmo2  8380  smores  8385  smores2  8387  dfrecs3  8405  naddunif  8728  ac6sfi  9300  fimaxg  9303  ordunifi  9306  isfinite2  9315  fipreima  9372  supisolem  9490  fiming  9516  infempty  9525  ordiso2  9533  ordtypelem7  9542  cantnf  9718  wemapwe  9722  rankval3b  9860  rankonidlem  9862  iscard  10080  acndom  10154  dfac12lem3  10248  kmlem2  10254  cflim2  10365  cfsmolem  10372  ttukeylem6  10616  alephreg  10691  suplem2pr  11162  axsup  11409  sup3  12298  infm3  12300  suprleub  12307  dfinfre  12322  infregelb  12325  ofsubeq0  12341  ofsubge0  12343  zextlt  12797  prime  12804  suprfinzcl  12837  indstr  13067  supxr2  13468  supxrbnd1  13475  supxrbnd2  13476  supxrleub  13480  supxrbnd  13482  infxrgelb  13490  fzshftral  13773  mptnn0fsupp  14164  swrdspsleq  14840  pfxeq  14870  clim  15687  rlim  15688  clim2  15697  clim2c  15698  clim0c  15700  ello1mpt  15714  lo1o1  15725  o1lo1  15730  climabs0  15778  o1compt  15780  rlimdiv  15839  geomulcvg  16071  mertenslem2  16080  mertens  16081  rpnnen2lem12  16419  sqrt2irr  16443  fprodfvdvdsd  16530  fproddvdsd  16531  dfgcd2  16745  isprm7  16910  pc11  17084  pcz  17085  1arith  17131  vdwlem8  17192  vdwlem11  17195  vdw  17198  ramval  17212  pwsle  17690  mrieqvd  17838  mreacs  17858  cidpropd  17910  ismon2  17935  monpropd  17938  isepi  17941  isepi2  17942  subsubc  18054  funcres2b  18098  funcpropd  18103  isfull2  18114  isfth2  18118  fucsect  18176  fucinv  18177  pospropd  18525  ipodrsfi  18739  tsrss  18789  grpidpropd  18868  mgmidpfod  18883  sgrppropd  18946  mndpropd  18977  smndex1mnd  19135  grppropd  19188  issubg4  19382  gass  19542  gsmsymgrfixlem1  19668  gsmsymgreqlem2  19672  gexdvds  19825  gexdvds2  19826  subgpgp  19838  sylow3lem6  19873  efgval2  19965  efgsp1  19978  dprdf11  20266  subgdmdprd  20277  rngpropd  20423  ringpropd  20546  isdrng5  21035  abvpropd  21119  lsspropd  21319  lbspropd  21401  isridlrng  21525  isridl  21572  phlpropd  21988  ishil2  22052  frlmplusgvalb  22102  frlmvscavalb  22103  frlmvplusgscavalb  22104  lindfmm  22160  islindf4  22171  islindf5  22172  assapropd  22206  psrbaglefi  22261  psrbagconf1o  22264  gsumbagdiaglem  22266  mplmonmul  22372  gsumply1eq  22654  scmatf1  22873  cpmatmcllem  23063  cpmatmcl  23064  decpmataa0  23113  decpmatmulsumfsupp  23118  pmatcollpw2lem  23122  pm2mpmhmlem1  23163  tgss2  23332  isclo  23432  neips  23458  opnnei  23465  isperf3  23498  ssidcn  23600  lmbrf  23605  cnnei  23627  cnrest2  23631  lmss  23643  lmres  23645  ist1-2  23692  ist1-3  23694  isreg2  23722  cmpfi  23753  bwth  23755  1stccn  23809  subislly  23827  kgencn  23902  ptclsg  23961  ptcnplem  23967  xkococnlem  24005  xkoinjcn  24033  tgqtop  24058  qtopcn  24060  fbflim  24322  flimrest  24329  flfnei  24337  isflf  24339  cnflf  24348  fclsopn  24360  fclsbas  24367  fclsrest  24370  isfcf  24380  cnfcf  24388  ptcmplem3  24400  tmdgsum2  24442  eltsms  24479  tsmsgsum  24485  tsmssubm  24489  tsmsf1o  24491  utopsnneiplem  24593  ismet2  24679  prdsxmetlem  24714  elmopn2  24791  prdsbl  24837  metss  24854  metrest  24870  metcnp  24887  metcnp2  24888  metcn  24889  metucn  24917  nrginvrcn  25038  metdsge  25196  divcn  25216  elcncf2  25238  mulc1cncf  25253  cncfmet  25257  evth2  25308  lmmbr2  25607  lmmbrf  25610  iscfil2  25614  cfil3i  25617  iscau2  25625  iscau4  25627  iscauf  25628  caucfil  25631  iscmet3lem3  25638  cfilres  25644  causs  25646  lmclim  25651  rrxmet  25756  evthicc2  25808  cniccbdd  25809  ovolfioo  25815  ovolficc  25816  ismbl2  25875  mbfsup  26012  mbfinf  26013  mbflimsup  26014  0plef  26020  mbfi1flim  26071  xrge0f  26079  itg2mulclem  26094  itgeqa  26161  ellimc2  26224  ellimc3  26226  limcflf  26228  cnlimc  26235  dvferm1  26332  dvferm2  26334  rolle  26337  dvivthlem1  26355  ftc1lem6  26388  itgsubst  26396  mdegle0  26422  deg1leb  26440  plydivex  26645  rnplynfin  26657  ulm2  26739  ulmcaulem  26748  ulmcau  26749  ulmdvlem3  26756  abelthlem9  26794  abelth  26795  rlimcnp  27320  ftalem3  27429  issqf  27490  sqf11  27493  mpodvdsmulf1o  27548  dvdsmulf1o  27550  dchrelbas4  27597  dchrinv  27615  2sqlem6  27777  chpo1ubb  27835  dchrmusumlema  27847  dchrisum0lema  27868  ostth3  27992  ltsrec  28214  lrrecfr  28356  addsuniflem  28414  addbday  28431  negsunif  28468  n0fincut  28768  bdayfinbndlem1  28880  elreno2  28908  tgcgr4  29021  eqeelen  29509  brbtwn2  29510  colinearalg  29515  axcgrid  29521  axsegconlem1  29522  ax5seglem4  29537  ax5seglem5  29538  axbtwnid  29544  axpasch  29546  axeuclidlem  29567  axcontlem2  29570  axcontlem4  29572  axcontlem7  29575  axcontlem12  29580  elntg2  29590  isuvtx  30003  uvtx2vtx1edg  30006  uvtx2vtx1edgb  30007  iscplgrnb  30024  iscplgredg  30025  vdiscusgrb  30138  uhgrvd00  30142  upgriswlk  30248  wwlksnext  30509  clwwlkinwwlk  30658  clwwlkel  30664  clwwlkf  30665  clwwlkwwlksb  30672  wwlksext2clwwlk  30675  wwlksubclwwlk  30676  clwwlknonex2lem2  30726  nmounbi  31405  blocnilem  31433  isph  31451  phoeqi  31486  h2hcau  31608  h2hlm  31609  hial2eq2  31736  hoeq1  32459  hoeq2  32460  adjsym  32462  cnvadj  32521  hhcno  32533  hhcnf  32534  adjvalval  32566  leop2  32753  leoptri  32765  mdbr2  32925  dmdbr2  32932  mddmd2  32938  cdj3lem3b  33069  infxrge0gelb  33425  prodindf  33496  toslublem  33600  tosglblem  33602  mgccnv  33627  cntrval2  33799  submarchi  33814  isarchi3  33815  lindfpropd  34004  opprlidlabs  34076  ply1moneq  34187  psrmonmul  34249  cmpcref  34549  lmdvg  34652  eulerpartlemd  35065  subfacp1lem3  36113  subfacp1lem5  36115  satfv1lem  36293  dfrdg2  36734  nadddilem2  37147  nadddilem4  37149  opnrebl  37285  poimirlem23  38752  broucube  38763  itg2gt0cn  38784  ftc1cnnc  38801  lmclim2  38883  caures  38885  sstotbnd2  38899  rrnmet  38954  rrncmslem  38957  isdrngo3  39084  isidlc  39140  cvrval2  40522  isat3  40555  iscvlat2N  40572  glbconN  40625  ltrneq  41397  cdlemefrs29clN  41647  cdlemefrs32fva  41648  cdleme32fva  41685  cdlemk33N  42157  cdlemk34  42158  cdlemkid3N  42181  cdlemkid4  42182  diaglbN  42303  dibglbN  42414  dihglbcpreN  42548  dihglblem6  42588  hdmap1eulem  43070  hdmap1eulemOLDN  43071  hdmapoc  43179  hlhilocv  43205  primrootsunit1  43338  sn-sup3d  43747  fimgmcyc  43789  wepwsolem  44240  islnm2  44271  onmaxnelsup  44415  onsupnmax  44420  onsupuni  44421  onsupmaxb  44431  onsupeqnmax  44439  iscard5  44727  alephiso2  44749  clsk3nimkb  45230  ntrclsneine0  45255  ntrneineine0  45277  ntrneineine1  45278  ntrneicls00  45279  ntrneicls11  45280  ntrneiiso  45281  ntrneik2  45282  ntrneix2  45283  ntrneikb  45284  ntrneixb  45285  ntrneik3  45286  ntrneix3  45287  ntrneik13  45288  ntrneix13  45289  ntrneik4w  45290  ntrneik4  45291  caofcan  45497  modelac8prim  46175  infxrbnd2  46583  supminfxr  46677  rexanuz2nf  46705  evthiccabs  46711  ellimcabssub0  46832  climf  46837  clim2f  46849  clim2cf  46863  clim0cf  46867  limsupmnflem  46933  limsupre2lem  46937  limsupreuzmpt  46952  supcnvlimsup  46953  limsupge  46974  liminfreuzlem  47015  liminfltlem  47017  liminflimsupclim  47020  liminfpnfuz  47029  xlimpnfxnegmnf2  47071  fourierdlem70  47389  fourierdlem71  47390  fourierdlem73  47392  fourierdlem80  47399  fourierdlem83  47402  fourierdlem87  47406  voliunsge0lem  47685  meaiuninclem  47693  meaiuninc3v  47697  hoidmv1lelem3  47806  hoidmvlelem4  47811  hoidmvlelem5  47812  issmflem  47940  chnerlem1  48095  cfsetsnfsetf  48331  cfsetsnfsetfo  48333  nprmmul1  48812  requad2  48924  isubgrgrim  49230  grlicref  49313  islinindfis  49764  elbigolo1  49872  line2x  50069  itscnhlinecirc02p  50100  iscnrm3lem1  50251  ipolublem  50303  ipoglblem  50306  oppcup  50526  uptrlem3  50531  natideq  50548  natcoeq  50549  fucidcobi  50550  initopropd  50568  termopropd  50569  fucoisfunc2lem1  50691  isinito2lem  50836  termc2  50856  lanup  51027  ranup  51028  aacllem  51217