Theorem ralbidva 3174

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3061

This theorem is referenced by:  ralbidv  3176  2ralbidva  3215  raleqbidva  3326  poinxp  5748  soinxp  5749  frinxp  5750  ordunisssuc  6459  fnmptfvd  7027  funimass3  7040  fnnfpeq0  7160  cocan1  7273  cocan2  7274  isores2  7314  isoini2  7320  ofrfvalg  7661  ofrfval2  7674  tfindsg2  7834  f1oweALT  7941  fnsuppres  8158  dfsmo2  8329  smores  8334  smores2  8336  dfrecs3  8354  dfrecs3OLD  8355  naddunif  8675  ac6sfi  9270  fimaxg  9273  ordunifi  9276  isfinite2  9284  fipreima  9341  supisolem  9450  fiming  9475  infempty  9484  ordiso2  9492  ordtypelem7  9501  cantnf  9670  wemapwe  9674  rankval3b  9803  rankonidlem  9805  iscard  9952  acndom  10028  dfac12lem3  10122  kmlem2  10128  cflim2  10240  cfsmolem  10247  ttukeylem6  10491  alephreg  10559  suplem2pr  11030  axsup  11271  sup3  12153  infm3  12155  suprleub  12162  dfinfre  12177  infregelb  12180  ofsubeq0  12191  ofsubge0  12193  zextlt  12618  prime  12625  suprfinzcl  12658  indstr  12882  supxr2  13275  supxrbnd1  13282  supxrbnd2  13283  supxrleub  13287  supxrbnd  13289  infxrgelb  13296  fzshftral  13571  mptnn0fsupp  13944  swrdspsleq  14597  pfxeq  14628  clim  15420  rlim  15421  clim2  15430  clim2c  15431  clim0c  15433  ello1mpt  15447  lo1o1  15458  o1lo1  15463  climabs0  15511  o1compt  15513  rlimdiv  15574  geomulcvg  15804  mertenslem2  15813  mertens  15814  rpnnen2lem12  16150  sqrt2irr  16174  fprodfvdvdsd  16259  fproddvdsd  16260  dfgcd2  16470  isprm7  16627  pc11  16795  pcz  16796  1arith  16842  vdwlem8  16903  vdwlem11  16906  vdw  16909  ramval  16923  pwsle  17420  mrieqvd  17564  mreacs  17584  cidpropd  17636  ismon2  17663  monpropd  17666  isepi  17669  isepi2  17670  subsubc  17785  funcres2b  17829  funcpropd  17833  isfull2  17844  isfth2  17848  fucsect  17907  fucinv  17908  pospropd  18262  ipodrsfi  18474  tsrss  18524  grpidpropd  18563  mndpropd  18627  smndex1mnd  18766  grppropd  18812  issubg4  18997  gass  19131  gsmsymgrfixlem1  19259  gsmsymgreqlem2  19263  gexdvds  19416  gexdvds2  19417  subgpgp  19429  sylow3lem6  19464  efgval2  19556  efgsp1  19569  dprdf11  19852  subgdmdprd  19863  ringpropd  20059  abvpropd  20399  lsspropd  20577  lbspropd  20659  phlpropd  21141  ishil2  21207  frlmplusgvalb  21257  frlmvscavalb  21258  frlmvplusgscavalb  21259  lindfmm  21315  islindf4  21326  islindf5  21327  assapropd  21357  psrbaglefi  21416  psrbaglefiOLD  21417  psrbagconf1o  21420  psrbagconf1oOLD  21421  gsumbagdiaglemOLD  21422  gsumbagdiaglem  21425  mplmonmul  21519  gsumply1eq  21758  scmatf1  21962  cpmatmcllem  22149  cpmatmcl  22150  decpmataa0  22199  decpmatmulsumfsupp  22204  pmatcollpw2lem  22208  pm2mpmhmlem1  22249  tgss2  22419  isclo  22520  neips  22546  opnnei  22553  isperf3  22586  ssidcn  22688  lmbrf  22693  cnnei  22715  cnrest2  22719  lmss  22731  lmres  22733  ist1-2  22780  ist1-3  22782  isreg2  22810  cmpfi  22841  bwth  22843  1stccn  22896  subislly  22914  kgencn  22989  ptclsg  23048  ptcnplem  23054  xkococnlem  23092  xkoinjcn  23120  tgqtop  23145  qtopcn  23147  fbflim  23409  flimrest  23416  flfnei  23424  isflf  23426  cnflf  23435  fclsopn  23447  fclsbas  23454  fclsrest  23457  isfcf  23467  cnfcf  23475  ptcmplem3  23487  tmdgsum2  23529  eltsms  23566  tsmsgsum  23572  tsmssubm  23576  tsmsf1o  23578  utopsnneiplem  23681  ismet2  23768  prdsxmetlem  23803  elmopn2  23880  prdsbl  23929  metss  23946  metrest  23962  metcnp  23979  metcnp2  23980  metcn  23981  metucn  24009  nrginvrcn  24138  metdsge  24294  divcn  24313  elcncf2  24335  mulc1cncf  24350  cncfmet  24354  evth2  24405  lmmbr2  24705  lmmbrf  24708  iscfil2  24712  cfil3i  24715  iscau2  24723  iscau4  24725  iscauf  24726  caucfil  24729  iscmet3lem3  24736  cfilres  24742  causs  24744  lmclim  24749  rrxmet  24854  evthicc2  24906  cniccbdd  24907  ovolfioo  24913  ovolficc  24914  ismbl2  24973  mbfsup  25110  mbfinf  25111  mbflimsup  25112  0plef  25118  mbfi1flim  25170  xrge0f  25178  itg2mulclem  25193  itgeqa  25260  ellimc2  25323  ellimc3  25325  limcflf  25327  cnlimc  25334  dvferm1  25431  dvferm2  25433  rolle  25436  dvivthlem1  25454  ftc1lem6  25487  itgsubst  25495  mdegle0  25524  deg1leb  25542  plydivex  25739  ulm2  25826  ulmcaulem  25835  ulmcau  25836  ulmdvlem3  25843  abelthlem9  25881  abelth  25882  rlimcnp  26397  ftalem3  26506  issqf  26567  sqf11  26570  dvdsmulf1o  26625  dchrelbas4  26673  dchrinv  26691  2sqlem6  26853  chpo1ubb  26911  dchrmusumlema  26923  dchrisum0lema  26944  ostth3  27068  sltrec  27247  lrrecfr  27343  addsuniflem  27400  negsunif  27443  tgcgr4  27647  eqeelen  28027  brbtwn2  28028  colinearalg  28033  axcgrid  28039  axsegconlem1  28040  ax5seglem4  28055  ax5seglem5  28056  axbtwnid  28062  axpasch  28064  axeuclidlem  28085  axcontlem2  28088  axcontlem4  28090  axcontlem7  28093  axcontlem12  28098  elntg2  28108  isuvtx  28517  uvtx2vtx1edg  28520  uvtx2vtx1edgb  28521  iscplgrnb  28538  iscplgredg  28539  vdiscusgrb  28652  uhgrvd00  28656  upgriswlk  28763  wwlksnext  29012  clwwlkinwwlk  29158  clwwlkel  29164  clwwlkf  29165  clwwlkwwlksb  29172  wwlksext2clwwlk  29175  wwlksubclwwlk  29176  clwwlknonex2lem2  29226  nmounbi  29892  blocnilem  29920  isph  29938  phoeqi  29973  h2hcau  30095  h2hlm  30096  hial2eq2  30223  hoeq1  30946  hoeq2  30947  adjsym  30949  cnvadj  31008  hhcno  31020  hhcnf  31021  adjvalval  31053  leop2  31240  leoptri  31252  mdbr2  31412  dmdbr2  31419  mddmd2  31425  cdj3lem3b  31556  infxrge0gelb  31850  toslublem  32013  tosglblem  32015  mgccnv  32040  submarchi  32203  isarchi3  32204  lindfpropd  32356  opprlidlabs  32445  ply1moneq  32505  cmpcref  32661  lmdvg  32764  prodindf  32852  eulerpartlemd  33196  subfacp1lem3  34004  subfacp1lem5  34006  satfv1lem  34184  dfrdg2  34597  opnrebl  35009  poimirlem23  36315  broucube  36326  itg2gt0cn  36347  ftc1cnnc  36364  lmclim2  36431  caures  36433  sstotbnd2  36447  rrnmet  36502  rrncmslem  36505  isdrngo3  36632  isidlc  36688  cvrval2  37949  isat3  37982  iscvlat2N  37999  glbconN  38052  glbconNOLD  38053  ltrneq  38825  cdlemefrs29clN  39075  cdlemefrs32fva  39076  cdleme32fva  39113  cdlemk33N  39585  cdlemk34  39586  cdlemkid3N  39609  cdlemkid4  39610  diaglbN  39731  dibglbN  39842  dihglbcpreN  39976  dihglblem6  40016  hdmap1eulem  40498  hdmap1eulemOLDN  40499  hdmapoc  40607  hlhilocv  40637  wepwsolem  41555  fnwe2lem2  41564  islnm2  41591  onmaxnelsup  41743  onsupnmax  41748  onsupuni  41749  onsupmaxb  41759  onsupeqnmax  41767  iscard5  42058  alephiso2  42080  clsk3nimkb  42562  ntrclsneine0  42587  ntrneineine0  42609  ntrneineine1  42610  ntrneicls00  42611  ntrneicls11  42612  ntrneiiso  42613  ntrneik2  42614  ntrneix2  42615  ntrneikb  42616  ntrneixb  42617  ntrneik3  42618  ntrneix3  42619  ntrneik13  42620  ntrneix13  42621  ntrneik4w  42622  ntrneik4  42623  caofcan  42853  infxrbnd2  43852  supminfxr  43947  rexanuz2nf  43976  evthiccabs  43982  ellimcabssub0  44106  climf  44111  clim2f  44125  clim2cf  44139  clim0cf  44143  limsupmnflem  44209  limsupre2lem  44213  limsupreuzmpt  44228  supcnvlimsup  44229  limsupge  44250  liminfreuzlem  44291  liminfltlem  44293  liminflimsupclim  44296  liminfpnfuz  44305  xlimpnfxnegmnf2  44347  fourierdlem70  44665  fourierdlem71  44666  fourierdlem73  44668  fourierdlem80  44675  fourierdlem83  44678  fourierdlem87  44682  voliunsge0lem  44961  meaiuninclem  44969  meaiuninc3v  44973  hoidmv1lelem3  45082  hoidmvlelem4  45087  hoidmvlelem5  45088  issmflem  45216  cfsetsnfsetf  45540  cfsetsnfsetfo  45542  requad2  46063  islinindfis  46778  elbigolo1  46891  line2x  47088  itscnhlinecirc02p  47119  iscnrm3lem1  47214  ipolublem  47259  ipoglblem  47262  aacllem  47496