Theorem ralbidva 3154

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 803	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜒)))
3	2	ralbidv2 3152	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  ralbidv  3156  2ralbidva  3197  raleqbidva  3302  poinxp  5712  soinxp  5713  frinxp  5714  ordunisssuc  6428  fnmptfvd  6995  funimass3  7008  fnnfpeq0  7134  cocan1  7248  cocan2  7249  isores2  7290  isoini2  7296  ofrfvalg  7641  ofrfval2  7654  caofidlcan  7671  tfindsg2  7818  f1oweALT  7930  fnsuppres  8147  dfsmo2  8293  smores  8298  smores2  8300  dfrecs3  8318  naddunif  8634  ac6sfi  9207  fimaxg  9210  ordunifi  9213  isfinite2  9221  fipreima  9285  supisolem  9401  fiming  9427  infempty  9436  ordiso2  9444  ordtypelem7  9453  cantnf  9622  wemapwe  9626  rankval3b  9755  rankonidlem  9757  iscard  9904  acndom  9980  dfac12lem3  10075  kmlem2  10081  cflim2  10192  cfsmolem  10199  ttukeylem6  10443  alephreg  10511  suplem2pr  10982  axsup  11225  sup3  12116  infm3  12118  suprleub  12125  dfinfre  12140  infregelb  12143  ofsubeq0  12159  ofsubge0  12161  zextlt  12584  prime  12591  suprfinzcl  12624  indstr  12851  supxr2  13250  supxrbnd1  13257  supxrbnd2  13258  supxrleub  13262  supxrbnd  13264  infxrgelb  13272  fzshftral  13552  mptnn0fsupp  13938  swrdspsleq  14606  pfxeq  14637  clim  15436  rlim  15437  clim2  15446  clim2c  15447  clim0c  15449  ello1mpt  15463  lo1o1  15474  o1lo1  15479  climabs0  15527  o1compt  15529  rlimdiv  15588  geomulcvg  15818  mertenslem2  15827  mertens  15828  rpnnen2lem12  16169  sqrt2irr  16193  fprodfvdvdsd  16280  fproddvdsd  16281  dfgcd2  16492  isprm7  16654  pc11  16827  pcz  16828  1arith  16874  vdwlem8  16935  vdwlem11  16938  vdw  16941  ramval  16955  pwsle  17431  mrieqvd  17579  mreacs  17599  cidpropd  17651  ismon2  17676  monpropd  17679  isepi  17682  isepi2  17683  subsubc  17795  funcres2b  17839  funcpropd  17844  isfull2  17855  isfth2  17859  fucsect  17917  fucinv  17918  pospropd  18266  ipodrsfi  18480  tsrss  18530  grpidpropd  18571  sgrppropd  18640  mndpropd  18668  smndex1mnd  18819  grppropd  18865  issubg4  19059  gass  19215  gsmsymgrfixlem1  19341  gsmsymgreqlem2  19345  gexdvds  19498  gexdvds2  19499  subgpgp  19511  sylow3lem6  19546  efgval2  19638  efgsp1  19651  dprdf11  19939  subgdmdprd  19950  rngpropd  20094  ringpropd  20208  abvpropd  20755  lsspropd  20956  lbspropd  21038  isridlrng  21161  isridl  21194  phlpropd  21597  ishil2  21661  frlmplusgvalb  21711  frlmvscavalb  21712  frlmvplusgscavalb  21713  lindfmm  21769  islindf4  21780  islindf5  21781  assapropd  21814  psrbaglefi  21868  psrbagconf1o  21871  gsumbagdiaglem  21872  mplmonmul  21976  gsumply1eq  22229  scmatf1  22451  cpmatmcllem  22638  cpmatmcl  22639  decpmataa0  22688  decpmatmulsumfsupp  22693  pmatcollpw2lem  22697  pm2mpmhmlem1  22738  tgss2  22907  isclo  23007  neips  23033  opnnei  23040  isperf3  23073  ssidcn  23175  lmbrf  23180  cnnei  23202  cnrest2  23206  lmss  23218  lmres  23220  ist1-2  23267  ist1-3  23269  isreg2  23297  cmpfi  23328  bwth  23330  1stccn  23383  subislly  23401  kgencn  23476  ptclsg  23535  ptcnplem  23541  xkococnlem  23579  xkoinjcn  23607  tgqtop  23632  qtopcn  23634  fbflim  23896  flimrest  23903  flfnei  23911  isflf  23913  cnflf  23922  fclsopn  23934  fclsbas  23941  fclsrest  23944  isfcf  23954  cnfcf  23962  ptcmplem3  23974  tmdgsum2  24016  eltsms  24053  tsmsgsum  24059  tsmssubm  24063  tsmsf1o  24065  utopsnneiplem  24168  ismet2  24254  prdsxmetlem  24289  elmopn2  24366  prdsbl  24412  metss  24429  metrest  24445  metcnp  24462  metcnp2  24463  metcn  24464  metucn  24492  nrginvrcn  24613  metdsge  24771  divcnOLD  24790  divcn  24792  elcncf2  24816  mulc1cncf  24831  cncfmet  24835  evth2  24892  lmmbr2  25192  lmmbrf  25195  iscfil2  25199  cfil3i  25202  iscau2  25210  iscau4  25212  iscauf  25213  caucfil  25216  iscmet3lem3  25223  cfilres  25229  causs  25231  lmclim  25236  rrxmet  25341  evthicc2  25394  cniccbdd  25395  ovolfioo  25401  ovolficc  25402  ismbl2  25461  mbfsup  25598  mbfinf  25599  mbflimsup  25600  0plef  25606  mbfi1flim  25657  xrge0f  25665  itg2mulclem  25680  itgeqa  25748  ellimc2  25811  ellimc3  25813  limcflf  25815  cnlimc  25822  dvferm1  25922  dvferm2  25924  rolle  25927  dvivthlem1  25946  ftc1lem6  25981  itgsubst  25989  mdegle0  26015  deg1leb  26033  plydivex  26238  ulm2  26327  ulmcaulem  26336  ulmcau  26337  ulmdvlem3  26344  abelthlem9  26383  abelth  26384  rlimcnp  26908  ftalem3  27018  issqf  27079  sqf11  27082  mpodvdsmulf1o  27137  dvdsmulf1o  27139  dchrelbas4  27187  dchrinv  27205  2sqlem6  27367  chpo1ubb  27425  dchrmusumlema  27437  dchrisum0lema  27458  ostth3  27582  sltrec  27767  lrrecfr  27890  addsuniflem  27948  addsbday  27964  negsunif  28001  n0sfincut  28286  tgcgr4  28511  eqeelen  28884  brbtwn2  28885  colinearalg  28890  axcgrid  28896  axsegconlem1  28897  ax5seglem4  28912  ax5seglem5  28913  axbtwnid  28919  axpasch  28921  axeuclidlem  28942  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  axcontlem12  28955  elntg2  28965  isuvtx  29375  uvtx2vtx1edg  29378  uvtx2vtx1edgb  29379  iscplgrnb  29396  iscplgredg  29397  vdiscusgrb  29511  uhgrvd00  29515  upgriswlk  29621  wwlksnext  29873  clwwlkinwwlk  30019  clwwlkel  30025  clwwlkf  30026  clwwlkwwlksb  30033  wwlksext2clwwlk  30036  wwlksubclwwlk  30037  clwwlknonex2lem2  30087  nmounbi  30755  blocnilem  30783  isph  30801  phoeqi  30836  h2hcau  30958  h2hlm  30959  hial2eq2  31086  hoeq1  31809  hoeq2  31810  adjsym  31812  cnvadj  31871  hhcno  31883  hhcnf  31884  adjvalval  31916  leop2  32103  leoptri  32115  mdbr2  32275  dmdbr2  32282  mddmd2  32288  cdj3lem3b  32419  infxrge0gelb  32739  prodindf  32836  toslublem  32944  tosglblem  32946  mgccnv  32971  cntrval2  33143  submarchi  33155  isarchi3  33156  lindfpropd  33346  opprlidlabs  33449  ply1moneq  33548  cmpcref  33833  lmdvg  33936  eulerpartlemd  34350  subfacp1lem3  35162  subfacp1lem5  35164  satfv1lem  35342  dfrdg2  35776  opnrebl  36301  poimirlem23  37630  broucube  37641  itg2gt0cn  37662  ftc1cnnc  37679  lmclim2  37745  caures  37747  sstotbnd2  37761  rrnmet  37816  rrncmslem  37819  isdrngo3  37946  isidlc  38002  cvrval2  39260  isat3  39293  iscvlat2N  39310  glbconN  39363  glbconNOLD  39364  ltrneq  40136  cdlemefrs29clN  40386  cdlemefrs32fva  40387  cdleme32fva  40424  cdlemk33N  40896  cdlemk34  40897  cdlemkid3N  40920  cdlemkid4  40921  diaglbN  41042  dibglbN  41153  dihglbcpreN  41287  dihglblem6  41327  hdmap1eulem  41809  hdmap1eulemOLDN  41810  hdmapoc  41918  hlhilocv  41944  primrootsunit1  42078  sn-sup3d  42473  fimgmcyc  42515  wepwsolem  43024  fnwe2lem2  43033  islnm2  43060  onmaxnelsup  43205  onsupnmax  43210  onsupuni  43211  onsupmaxb  43221  onsupeqnmax  43229  iscard5  43518  alephiso2  43540  clsk3nimkb  44022  ntrclsneine0  44047  ntrneineine0  44069  ntrneineine1  44070  ntrneicls00  44071  ntrneicls11  44072  ntrneiiso  44073  ntrneik2  44074  ntrneix2  44075  ntrneikb  44076  ntrneixb  44077  ntrneik3  44078  ntrneix3  44079  ntrneik13  44080  ntrneix13  44081  ntrneik4w  44082  ntrneik4  44083  caofcan  44305  modelac8prim  44975  infxrbnd2  45358  supminfxr  45453  rexanuz2nf  45481  evthiccabs  45487  ellimcabssub0  45608  climf  45613  clim2f  45627  clim2cf  45641  clim0cf  45645  limsupmnflem  45711  limsupre2lem  45715  limsupreuzmpt  45730  supcnvlimsup  45731  limsupge  45752  liminfreuzlem  45793  liminfltlem  45795  liminflimsupclim  45798  liminfpnfuz  45807  xlimpnfxnegmnf2  45849  fourierdlem70  46167  fourierdlem71  46168  fourierdlem73  46170  fourierdlem80  46177  fourierdlem83  46180  fourierdlem87  46184  voliunsge0lem  46463  meaiuninclem  46471  meaiuninc3v  46475  hoidmv1lelem3  46584  hoidmvlelem4  46589  hoidmvlelem5  46590  issmflem  46718  cfsetsnfsetf  47052  cfsetsnfsetfo  47054  requad2  47617  isubgrgrim  47922  grlicref  47997  islinindfis  48431  elbigolo1  48539  line2x  48736  itscnhlinecirc02p  48767  iscnrm3lem1  48915  ipolublem  48967  ipoglblem  48970  oppcup  49189  uptrlem3  49194  initopropd  49225  termopropd  49226  isinito2lem  49480  termc2  49500  lanup  49623  ranup  49624  aacllem  49783