Theorem ralbidva 3140

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∈ wcel 2048  ∀wral 3082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ral 3087

This theorem is referenced by:  ralbidv  3141  2ralbidva  3142  raleqbidva  3359  poinxp  5475  soinxp  5476  frinxp  5477  ordunisssuc  6125  fnmptfvd  6630  funimass3  6643  fnnfpeq0  6757  cocan1  6866  cocan2  6867  isores2  6903  isoini2  6909  ofrfval  7229  ofrfval2  7239  tfindsg2  7386  f1oweALT  7478  fnsuppres  7653  dfsmo2  7781  smores  7786  smores2  7788  dfrecs3  7806  ac6sfi  8549  fimaxg  8552  ordunifi  8555  isfinite2  8563  fipreima  8617  supisolem  8724  fiming  8749  infempty  8758  ordiso2  8766  ordtypelem7  8775  cantnf  8942  wemapwe  8946  rankval3b  9041  rankonidlem  9043  iscard  9190  acndom  9263  dfac12lem3  9357  kmlem2  9363  cflim2  9475  cfsmolem  9482  ttukeylem6  9726  alephreg  9794  suplem2pr  10265  axsup  10508  sup3  11391  infm3  11393  suprleub  11400  dfinfre  11415  infregelb  11418  ofsubeq0  11428  ofsubge0  11430  zextlt  11862  prime  11869  suprfinzcl  11903  indstr  12123  supxr2  12516  supxrbnd1  12523  supxrbnd2  12524  supxrleub  12528  supxrbnd  12530  infxrgelb  12537  fzshftral  12804  mptnn0fsupp  13173  swrdeqOLD  13826  swrdspsleq  13832  pfxeq  13868  clim  14702  rlim  14703  clim2  14712  clim2c  14713  clim0c  14715  ello1mpt  14729  lo1o1  14740  o1lo1  14745  climabs0  14793  o1compt  14795  rlimdiv  14853  geomulcvg  15082  mertenslem2  15091  mertens  15092  rpnnen2lem12  15428  sqrt2irr  15452  fprodfvdvdsd  15533  fproddvdsd  15534  dfgcd2  15740  isprm7  15898  pc11  16062  pcz  16063  1arith  16109  vdwlem8  16170  vdwlem11  16173  vdw  16176  ramval  16190  pwsle  16611  mrieqvd  16757  mreacs  16777  cidpropd  16828  ismon2  16852  monpropd  16855  isepi  16858  isepi2  16859  subsubc  16971  funcres2b  17015  funcpropd  17018  isfull2  17029  isfth2  17033  fucsect  17090  fucinv  17091  pospropd  17592  ipodrsfi  17621  tsrss  17681  grpidpropd  17719  mndpropd  17774  grppropd  17896  issubg4  18072  gass  18192  gsmsymgrfixlem1  18306  gsmsymgreqlem2  18310  gexdvds  18460  gexdvds2  18461  subgpgp  18473  sylow3lem6  18508  efgval2  18598  efgsp1  18611  dprdf11  18885  subgdmdprd  18896  ringpropd  19045  abvpropd  19325  lsspropd  19501  lbspropd  19583  assapropd  19811  psrbaglefi  19856  psrbagconf1o  19858  gsumbagdiaglem  19859  mplmonmul  19948  gsumply1eq  20166  phlpropd  20491  ishil2  20555  frlmplusgvalb  20605  frlmvscavalb  20606  frlmvplusgscavalb  20607  lindfmm  20663  islindf4  20674  islindf5  20675  scmatf1  20834  cpmatmcllem  21020  cpmatmcl  21021  decpmataa0  21070  decpmatmulsumfsupp  21075  pmatcollpw2lem  21079  pm2mpmhmlem1  21120  tgss2  21289  isclo  21389  neips  21415  opnnei  21422  isperf3  21455  ssidcn  21557  lmbrf  21562  cnnei  21584  cnrest2  21588  lmss  21600  lmres  21602  ist1-2  21649  ist1-3  21651  isreg2  21679  cmpfi  21710  bwth  21712  1stccn  21765  subislly  21783  kgencn  21858  ptclsg  21917  ptcnplem  21923  xkococnlem  21961  xkoinjcn  21989  tgqtop  22014  qtopcn  22016  fbflim  22278  flimrest  22285  flfnei  22293  isflf  22295  cnflf  22304  fclsopn  22316  fclsbas  22323  fclsrest  22326  isfcf  22336  cnfcf  22344  ptcmplem3  22356  tmdgsum2  22398  eltsms  22434  tsmsgsum  22440  tsmssubm  22444  tsmsf1o  22446  utopsnneiplem  22549  ismet2  22636  prdsxmetlem  22671  elmopn2  22748  prdsbl  22794  metss  22811  metrest  22827  metcnp  22844  metcnp2  22845  metcn  22846  metucn  22874  nrginvrcn  22994  metdsge  23150  divcn  23169  elcncf2  23191  mulc1cncf  23206  cncfmet  23209  evth2  23257  lmmbr2  23555  lmmbrf  23558  iscfil2  23562  cfil3i  23565  iscau2  23573  iscau4  23575  iscauf  23576  caucfil  23579  iscmet3lem3  23586  cfilres  23592  causs  23594  lmclim  23599  rrxmet  23704  evthicc2  23754  cniccbdd  23755  ovolfioo  23761  ovolficc  23762  ismbl2  23821  mbfsup  23958  mbfinf  23959  mbflimsup  23960  0plef  23966  mbfi1flim  24017  xrge0f  24025  itg2mulclem  24040  itgeqa  24107  ellimc2  24168  ellimc3  24170  limcflf  24172  cnlimc  24179  dvferm1  24275  dvferm2  24277  rolle  24280  dvivthlem1  24298  ftc1lem6  24331  itgsubst  24339  mdegle0  24364  deg1leb  24382  plydivex  24579  ulm2  24666  ulmcaulem  24675  ulmcau  24676  ulmdvlem3  24683  abelthlem9  24721  abelth  24722  rlimcnp  25235  ftalem3  25344  issqf  25405  sqf11  25408  dvdsmulf1o  25463  dchrelbas4  25511  dchrinv  25529  2sqlem6  25691  chpo1ubb  25749  dchrmusumlema  25761  dchrisum0lema  25782  ostth3  25906  tgcgr4  26009  eqeelen  26383  brbtwn2  26384  colinearalg  26389  axcgrid  26395  axsegconlem1  26396  ax5seglem4  26411  ax5seglem5  26412  axbtwnid  26418  axpasch  26420  axeuclidlem  26441  axcontlem2  26444  axcontlem4  26446  axcontlem7  26449  axcontlem12  26454  elntg2  26464  isuvtx  26870  uvtx2vtx1edg  26873  uvtx2vtx1edgb  26874  iscplgrnb  26891  iscplgredg  26892  vdiscusgrb  27005  uhgrvd00  27009  upgriswlk  27115  wwlksnext  27371  clwwlkinwwlk  27545  clwwlkinwwlkOLD  27546  clwwlkel  27553  clwwlkfOLD  27554  clwwlkf  27559  clwwlkwwlksb  27567  wwlksext2clwwlk  27570  wwlksubclwwlk  27571  wwlksubclwwlkOLD  27572  clwwlknonex2lem2  27626  nmounbi  28320  blocnilem  28348  isph  28366  phoeqi  28402  h2hcau  28525  h2hlm  28526  hial2eq2  28653  hoeq1  29378  hoeq2  29379  adjsym  29381  cnvadj  29440  hhcno  29452  hhcnf  29453  adjvalval  29485  leop2  29672  leoptri  29684  mdbr2  29844  dmdbr2  29851  mddmd2  29857  cdj3lem3b  29988  infxrge0gelb  30231  toslublem  30364  tosglblem  30366  submarchi  30437  isarchi3  30438  lindfpropd  30569  cmpcref  30715  lmdvg  30797  prodindf  30883  eulerpartlemd  31226  subfacp1lem3  31974  subfacp1lem5  31976  dfrdg2  32501  sltrec  32739  opnrebl  33129  poimirlem23  34304  broucube  34315  itg2gt0cn  34336  ftc1cnnc  34355  lmclim2  34423  caures  34425  sstotbnd2  34442  rrnmet  34497  rrncmslem  34500  isdrngo3  34627  isidlc  34683  cvrval2  35803  isat3  35836  iscvlat2N  35853  glbconN  35906  ltrneq  36678  cdlemefrs29clN  36928  cdlemefrs32fva  36929  cdleme32fva  36966  cdlemk33N  37438  cdlemk34  37439  cdlemkid3N  37462  cdlemkid4  37463  diaglbN  37584  dibglbN  37695  dihglbcpreN  37829  dihglblem6  37869  hdmap1eulem  38351  hdmap1eulemOLDN  38352  hdmapoc  38460  hlhilocv  38486  wepwsolem  38983  fnwe2lem2  38992  islnm2  39019  clsk3nimkb  39698  ntrclsneine0  39723  ntrneineine0  39745  ntrneineine1  39746  ntrneicls00  39747  ntrneicls11  39748  ntrneiiso  39749  ntrneik2  39750  ntrneix2  39751  ntrneikb  39752  ntrneixb  39753  ntrneik3  39754  ntrneix3  39755  ntrneik13  39756  ntrneix13  39757  ntrneik4w  39758  ntrneik4  39759  caofcan  40015  infxrbnd2  41012  supminfxr  41117  evthiccabs  41148  ellimcabssub0  41275  climf  41280  clim2f  41294  clim2cf  41308  clim0cf  41312  limsupmnflem  41378  limsupre2lem  41382  limsupreuzmpt  41397  supcnvlimsup  41398  limsupge  41419  liminfreuzlem  41460  liminfltlem  41462  liminflimsupclim  41465  liminfpnfuz  41474  xlimpnfxnegmnf2  41516  fourierdlem70  41838  fourierdlem71  41839  fourierdlem73  41841  fourierdlem80  41848  fourierdlem83  41851  fourierdlem87  41855  voliunsge0lem  42131  meaiuninclem  42139  meaiuninc3v  42143  hoidmv1lelem3  42252  hoidmvlelem4  42257  hoidmvlelem5  42258  issmflem  42381  requad2  43096  islinindfis  43811  elbigolo1  43925  line2x  44049  itscnhlinecirc02p  44080  aacllem  44209