Theorem ralbidva 3185

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3079

This theorem is referenced by:  ralbidv  3187  2ralbidva  3226  raleqbidva  3328  poinxp  5730  soinxp  5731  frinxp  5732  ordunisssuc  6456  fnmptfvd  7024  funimass3  7037  fnnfpeq0  7164  cocan1  7277  cocan2  7278  isores2  7319  isoini2  7325  ofrfvalg  7670  ofrfval2  7683  caofidlcan  7700  tfindsg2  7844  f1oweALT  7955  fnsuppres  8173  dfsmo2  8320  smores  8325  smores2  8327  dfrecs3  8345  naddunif  8666  ac6sfi  9230  fimaxg  9233  ordunifi  9236  isfinite2  9244  fipreima  9303  supisolem  9422  fiming  9448  infempty  9457  ordiso2  9465  ordtypelem7  9474  cantnf  9650  wemapwe  9654  rankval3b  9786  rankonidlem  9788  iscard  9935  acndom  10009  dfac12lem3  10104  kmlem2  10110  cflim2  10222  cfsmolem  10229  ttukeylem6  10473  alephreg  10542  suplem2pr  11013  axsup  11260  sup3  12151  infm3  12153  suprleub  12160  dfinfre  12175  infregelb  12178  ofsubeq0  12194  ofsubge0  12196  zextlt  12649  prime  12656  suprfinzcl  12689  indstr  12919  supxr2  13319  supxrbnd1  13326  supxrbnd2  13327  supxrleub  13331  supxrbnd  13333  infxrgelb  13341  fzshftral  13622  mptnn0fsupp  14012  swrdspsleq  14681  pfxeq  14711  clim  15523  rlim  15524  clim2  15533  clim2c  15534  clim0c  15536  ello1mpt  15550  lo1o1  15561  o1lo1  15566  climabs0  15614  o1compt  15616  rlimdiv  15675  geomulcvg  15908  mertenslem2  15917  mertens  15918  rpnnen2lem12  16259  sqrt2irr  16283  fprodfvdvdsd  16370  fproddvdsd  16371  dfgcd2  16582  isprm7  16745  pc11  16918  pcz  16919  1arith  16965  vdwlem8  17026  vdwlem11  17029  vdw  17032  ramval  17046  pwsle  17524  mrieqvd  17672  mreacs  17692  cidpropd  17744  ismon2  17769  monpropd  17772  isepi  17775  isepi2  17776  subsubc  17888  funcres2b  17932  funcpropd  17937  isfull2  17948  isfth2  17952  fucsect  18010  fucinv  18011  pospropd  18359  ipodrsfi  18573  tsrss  18623  grpidpropd  18698  sgrppropd  18767  mndpropd  18795  smndex1mnd  18949  grppropd  18995  issubg4  19189  gass  19343  gsmsymgrfixlem1  19469  gsmsymgreqlem2  19473  gexdvds  19626  gexdvds2  19627  subgpgp  19639  sylow3lem6  19674  efgval2  19766  efgsp1  19779  dprdf11  20067  subgdmdprd  20078  rngpropd  20222  ringpropd  20340  abvpropd  20886  lsspropd  21086  lbspropd  21168  isridlrng  21291  isridl  21324  phlpropd  21709  ishil2  21773  frlmplusgvalb  21823  frlmvscavalb  21824  frlmvplusgscavalb  21825  lindfmm  21881  islindf4  21892  islindf5  21893  assapropd  21925  psrbaglefi  21980  psrbagconf1o  21983  gsumbagdiaglem  21985  mplmonmul  22091  gsumply1eq  22374  scmatf1  22593  cpmatmcllem  22780  cpmatmcl  22781  decpmataa0  22830  decpmatmulsumfsupp  22835  pmatcollpw2lem  22839  pm2mpmhmlem1  22880  tgss2  23049  isclo  23149  neips  23175  opnnei  23182  isperf3  23215  ssidcn  23317  lmbrf  23322  cnnei  23344  cnrest2  23348  lmss  23360  lmres  23362  ist1-2  23409  ist1-3  23411  isreg2  23439  cmpfi  23470  bwth  23472  1stccn  23525  subislly  23543  kgencn  23618  ptclsg  23677  ptcnplem  23683  xkococnlem  23721  xkoinjcn  23749  tgqtop  23774  qtopcn  23776  fbflim  24038  flimrest  24045  flfnei  24053  isflf  24055  cnflf  24064  fclsopn  24076  fclsbas  24083  fclsrest  24086  isfcf  24096  cnfcf  24104  ptcmplem3  24116  tmdgsum2  24158  eltsms  24195  tsmsgsum  24201  tsmssubm  24205  tsmsf1o  24207  utopsnneiplem  24309  ismet2  24395  prdsxmetlem  24430  elmopn2  24507  prdsbl  24553  metss  24570  metrest  24586  metcnp  24603  metcnp2  24604  metcn  24605  metucn  24633  nrginvrcn  24754  metdsge  24912  divcn  24932  elcncf2  24954  mulc1cncf  24969  cncfmet  24973  evth2  25024  lmmbr2  25323  lmmbrf  25326  iscfil2  25330  cfil3i  25333  iscau2  25341  iscau4  25343  iscauf  25344  caucfil  25347  iscmet3lem3  25354  cfilres  25360  causs  25362  lmclim  25367  rrxmet  25472  evthicc2  25524  cniccbdd  25525  ovolfioo  25531  ovolficc  25532  ismbl2  25591  mbfsup  25728  mbfinf  25729  mbflimsup  25730  0plef  25736  mbfi1flim  25787  xrge0f  25795  itg2mulclem  25810  itgeqa  25878  ellimc2  25941  ellimc3  25943  limcflf  25945  cnlimc  25952  dvferm1  26049  dvferm2  26051  rolle  26054  dvivthlem1  26072  ftc1lem6  26105  itgsubst  26113  mdegle0  26139  deg1leb  26157  plydivex  26363  ulm2  26450  ulmcaulem  26459  ulmcau  26460  ulmdvlem3  26467  abelthlem9  26505  abelth  26506  rlimcnp  27032  ftalem3  27141  issqf  27202  sqf11  27205  mpodvdsmulf1o  27260  dvdsmulf1o  27262  dchrelbas4  27309  dchrinv  27327  2sqlem6  27489  chpo1ubb  27547  dchrmusumlema  27559  dchrisum0lema  27580  ostth3  27704  ltsrec  27896  lrrecfr  28038  addsuniflem  28096  addbday  28113  negsunif  28150  n0fincut  28450  bdayfinbndlem1  28562  elreno2  28590  tgcgr4  28702  eqeelen  29107  brbtwn2  29108  colinearalg  29113  axcgrid  29119  axsegconlem1  29120  ax5seglem4  29135  ax5seglem5  29136  axbtwnid  29142  axpasch  29144  axeuclidlem  29165  axcontlem2  29168  axcontlem4  29170  axcontlem7  29173  axcontlem12  29178  elntg2  29188  isuvtx  29598  uvtx2vtx1edg  29601  uvtx2vtx1edgb  29602  iscplgrnb  29619  iscplgredg  29620  vdiscusgrb  29733  uhgrvd00  29737  upgriswlk  29843  wwlksnext  30095  clwwlkinwwlk  30244  clwwlkel  30250  clwwlkf  30251  clwwlkwwlksb  30258  wwlksext2clwwlk  30261  wwlksubclwwlk  30262  clwwlknonex2lem2  30312  nmounbi  30981  blocnilem  31009  isph  31027  phoeqi  31062  h2hcau  31184  h2hlm  31185  hial2eq2  31312  hoeq1  32035  hoeq2  32036  adjsym  32038  cnvadj  32097  hhcno  32109  hhcnf  32110  adjvalval  32142  leop2  32329  leoptri  32341  mdbr2  32501  dmdbr2  32508  mddmd2  32514  cdj3lem3b  32645  infxrge0gelb  32970  prodindf  33042  toslublem  33152  tosglblem  33154  mgccnv  33179  cntrval2  33353  submarchi  33368  isarchi3  33369  lindfpropd  33570  opprlidlabs  33675  ply1moneq  33786  psrmonmul  33849  cmpcref  34149  lmdvg  34252  eulerpartlemd  34665  subfacp1lem3  35537  subfacp1lem5  35539  satfv1lem  35717  dfrdg2  36148  opnrebl  36685  poimirlem23  38147  broucube  38158  itg2gt0cn  38179  ftc1cnnc  38196  lmclim2  38262  caures  38264  sstotbnd2  38278  rrnmet  38333  rrncmslem  38336  isdrngo3  38463  isidlc  38519  cvrval2  39903  isat3  39936  iscvlat2N  39953  glbconN  40006  ltrneq  40778  cdlemefrs29clN  41028  cdlemefrs32fva  41029  cdleme32fva  41066  cdlemk33N  41538  cdlemk34  41539  cdlemkid3N  41562  cdlemkid4  41563  diaglbN  41684  dibglbN  41795  dihglbcpreN  41929  dihglblem6  41969  hdmap1eulem  42451  hdmap1eulemOLDN  42452  hdmapoc  42560  hlhilocv  42586  primrootsunit1  42719  sn-sup3d  43119  fimgmcyc  43157  wepwsolem  43624  fnwe2lem2  43633  islnm2  43660  onmaxnelsup  43805  onsupnmax  43810  onsupuni  43811  onsupmaxb  43821  onsupeqnmax  43829  iscard5  44117  alephiso2  44139  clsk3nimkb  44621  ntrclsneine0  44646  ntrneineine0  44668  ntrneineine1  44669  ntrneicls00  44670  ntrneicls11  44671  ntrneiiso  44672  ntrneik2  44673  ntrneix2  44674  ntrneikb  44675  ntrneixb  44676  ntrneik3  44677  ntrneix3  44678  ntrneik13  44679  ntrneix13  44680  ntrneik4w  44681  ntrneik4  44682  caofcan  44904  modelac8prim  45573  infxrbnd2  45949  supminfxr  46043  rexanuz2nf  46071  evthiccabs  46077  ellimcabssub0  46198  climf  46203  clim2f  46215  clim2cf  46229  clim0cf  46233  limsupmnflem  46299  limsupre2lem  46303  limsupreuzmpt  46318  supcnvlimsup  46319  limsupge  46340  liminfreuzlem  46381  liminfltlem  46383  liminflimsupclim  46386  liminfpnfuz  46395  xlimpnfxnegmnf2  46437  fourierdlem70  46755  fourierdlem71  46756  fourierdlem73  46758  fourierdlem80  46765  fourierdlem83  46768  fourierdlem87  46772  voliunsge0lem  47051  meaiuninclem  47059  meaiuninc3v  47063  hoidmv1lelem3  47172  hoidmvlelem4  47177  hoidmvlelem5  47178  issmflem  47306  chnerlem1  47463  cfsetsnfsetf  47657  cfsetsnfsetfo  47659  nprmmul1  48138  requad2  48250  isubgrgrim  48556  grlicref  48639  islinindfis  49076  elbigolo1  49184  line2x  49381  itscnhlinecirc02p  49412  iscnrm3lem1  49560  ipolublem  49612  ipoglblem  49615  oppcup  49833  uptrlem3  49838  initopropd  49869  termopropd  49870  isinito2lem  50124  termc2  50144  lanup  50267  ranup  50268  aacllem  50427