Theorem ralbidva 3173

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∈ wcel 2104  ∀wral 3059

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  ralbidv  3175  2ralbidva  3214  raleqbidva  3325  poinxp  5755  soinxp  5756  frinxp  5757  ordunisssuc  6469  fnmptfvd  7041  funimass3  7054  fnnfpeq0  7177  cocan1  7291  cocan2  7292  isores2  7332  isoini2  7338  ofrfvalg  7680  ofrfval2  7693  tfindsg2  7853  f1oweALT  7961  fnsuppres  8178  dfsmo2  8349  smores  8354  smores2  8356  dfrecs3  8374  dfrecs3OLD  8375  naddunif  8694  ac6sfi  9289  fimaxg  9292  ordunifi  9295  isfinite2  9303  fipreima  9360  supisolem  9470  fiming  9495  infempty  9504  ordiso2  9512  ordtypelem7  9521  cantnf  9690  wemapwe  9694  rankval3b  9823  rankonidlem  9825  iscard  9972  acndom  10048  dfac12lem3  10142  kmlem2  10148  cflim2  10260  cfsmolem  10267  ttukeylem6  10511  alephreg  10579  suplem2pr  11050  axsup  11293  sup3  12175  infm3  12177  suprleub  12184  dfinfre  12199  infregelb  12202  ofsubeq0  12213  ofsubge0  12215  zextlt  12640  prime  12647  suprfinzcl  12680  indstr  12904  supxr2  13297  supxrbnd1  13304  supxrbnd2  13305  supxrleub  13309  supxrbnd  13311  infxrgelb  13318  fzshftral  13593  mptnn0fsupp  13966  swrdspsleq  14619  pfxeq  14650  clim  15442  rlim  15443  clim2  15452  clim2c  15453  clim0c  15455  ello1mpt  15469  lo1o1  15480  o1lo1  15485  climabs0  15533  o1compt  15535  rlimdiv  15596  geomulcvg  15826  mertenslem2  15835  mertens  15836  rpnnen2lem12  16172  sqrt2irr  16196  fprodfvdvdsd  16281  fproddvdsd  16282  dfgcd2  16492  isprm7  16649  pc11  16817  pcz  16818  1arith  16864  vdwlem8  16925  vdwlem11  16928  vdw  16931  ramval  16945  pwsle  17442  mrieqvd  17586  mreacs  17606  cidpropd  17658  ismon2  17685  monpropd  17688  isepi  17691  isepi2  17692  subsubc  17807  funcres2b  17851  funcpropd  17855  isfull2  17866  isfth2  17870  fucsect  17929  fucinv  17930  pospropd  18284  ipodrsfi  18496  tsrss  18546  grpidpropd  18587  sgrppropd  18656  mndpropd  18684  smndex1mnd  18827  grppropd  18873  issubg4  19061  gass  19206  gsmsymgrfixlem1  19336  gsmsymgreqlem2  19340  gexdvds  19493  gexdvds2  19494  subgpgp  19506  sylow3lem6  19541  efgval2  19633  efgsp1  19646  dprdf11  19934  subgdmdprd  19945  rngpropd  20068  ringpropd  20176  abvpropd  20593  lsspropd  20772  lbspropd  20854  isridl  21008  isridlrng  21031  phlpropd  21427  ishil2  21493  frlmplusgvalb  21543  frlmvscavalb  21544  frlmvplusgscavalb  21545  lindfmm  21601  islindf4  21612  islindf5  21613  assapropd  21645  psrbaglefi  21704  psrbaglefiOLD  21705  psrbagconf1o  21708  psrbagconf1oOLD  21709  gsumbagdiaglemOLD  21710  gsumbagdiaglem  21713  mplmonmul  21810  gsumply1eq  22049  scmatf1  22253  cpmatmcllem  22440  cpmatmcl  22441  decpmataa0  22490  decpmatmulsumfsupp  22495  pmatcollpw2lem  22499  pm2mpmhmlem1  22540  tgss2  22710  isclo  22811  neips  22837  opnnei  22844  isperf3  22877  ssidcn  22979  lmbrf  22984  cnnei  23006  cnrest2  23010  lmss  23022  lmres  23024  ist1-2  23071  ist1-3  23073  isreg2  23101  cmpfi  23132  bwth  23134  1stccn  23187  subislly  23205  kgencn  23280  ptclsg  23339  ptcnplem  23345  xkococnlem  23383  xkoinjcn  23411  tgqtop  23436  qtopcn  23438  fbflim  23700  flimrest  23707  flfnei  23715  isflf  23717  cnflf  23726  fclsopn  23738  fclsbas  23745  fclsrest  23748  isfcf  23758  cnfcf  23766  ptcmplem3  23778  tmdgsum2  23820  eltsms  23857  tsmsgsum  23863  tsmssubm  23867  tsmsf1o  23869  utopsnneiplem  23972  ismet2  24059  prdsxmetlem  24094  elmopn2  24171  prdsbl  24220  metss  24237  metrest  24253  metcnp  24270  metcnp2  24271  metcn  24272  metucn  24300  nrginvrcn  24429  metdsge  24585  divcnOLD  24604  divcn  24606  elcncf2  24630  mulc1cncf  24645  cncfmet  24649  evth2  24706  lmmbr2  25007  lmmbrf  25010  iscfil2  25014  cfil3i  25017  iscau2  25025  iscau4  25027  iscauf  25028  caucfil  25031  iscmet3lem3  25038  cfilres  25044  causs  25046  lmclim  25051  rrxmet  25156  evthicc2  25209  cniccbdd  25210  ovolfioo  25216  ovolficc  25217  ismbl2  25276  mbfsup  25413  mbfinf  25414  mbflimsup  25415  0plef  25421  mbfi1flim  25473  xrge0f  25481  itg2mulclem  25496  itgeqa  25563  ellimc2  25626  ellimc3  25628  limcflf  25630  cnlimc  25637  dvferm1  25737  dvferm2  25739  rolle  25742  dvivthlem1  25760  ftc1lem6  25793  itgsubst  25801  mdegle0  25830  deg1leb  25848  plydivex  26046  ulm2  26133  ulmcaulem  26142  ulmcau  26143  ulmdvlem3  26150  abelthlem9  26188  abelth  26189  rlimcnp  26706  ftalem3  26815  issqf  26876  sqf11  26879  dvdsmulf1o  26934  dchrelbas4  26982  dchrinv  27000  2sqlem6  27162  chpo1ubb  27220  dchrmusumlema  27232  dchrisum0lema  27253  ostth3  27377  sltrec  27558  lrrecfr  27665  addsuniflem  27723  negsunif  27768  tgcgr4  28049  eqeelen  28429  brbtwn2  28430  colinearalg  28435  axcgrid  28441  axsegconlem1  28442  ax5seglem4  28457  ax5seglem5  28458  axbtwnid  28464  axpasch  28466  axeuclidlem  28487  axcontlem2  28490  axcontlem4  28492  axcontlem7  28495  axcontlem12  28500  elntg2  28510  isuvtx  28919  uvtx2vtx1edg  28922  uvtx2vtx1edgb  28923  iscplgrnb  28940  iscplgredg  28941  vdiscusgrb  29054  uhgrvd00  29058  upgriswlk  29165  wwlksnext  29414  clwwlkinwwlk  29560  clwwlkel  29566  clwwlkf  29567  clwwlkwwlksb  29574  wwlksext2clwwlk  29577  wwlksubclwwlk  29578  clwwlknonex2lem2  29628  nmounbi  30296  blocnilem  30324  isph  30342  phoeqi  30377  h2hcau  30499  h2hlm  30500  hial2eq2  30627  hoeq1  31350  hoeq2  31351  adjsym  31353  cnvadj  31412  hhcno  31424  hhcnf  31425  adjvalval  31457  leop2  31644  leoptri  31656  mdbr2  31816  dmdbr2  31823  mddmd2  31829  cdj3lem3b  31960  infxrge0gelb  32246  toslublem  32409  tosglblem  32411  mgccnv  32436  submarchi  32602  isarchi3  32603  lindfpropd  32772  opprlidlabs  32873  ply1moneq  32939  cmpcref  33128  lmdvg  33231  prodindf  33319  eulerpartlemd  33663  subfacp1lem3  34471  subfacp1lem5  34473  satfv1lem  34651  dfrdg2  35071  opnrebl  35508  poimirlem23  36814  broucube  36825  itg2gt0cn  36846  ftc1cnnc  36863  lmclim2  36929  caures  36931  sstotbnd2  36945  rrnmet  37000  rrncmslem  37003  isdrngo3  37130  isidlc  37186  cvrval2  38447  isat3  38480  iscvlat2N  38497  glbconN  38550  glbconNOLD  38551  ltrneq  39323  cdlemefrs29clN  39573  cdlemefrs32fva  39574  cdleme32fva  39611  cdlemk33N  40083  cdlemk34  40084  cdlemkid3N  40107  cdlemkid4  40108  diaglbN  40229  dibglbN  40340  dihglbcpreN  40474  dihglblem6  40514  hdmap1eulem  40996  hdmap1eulemOLDN  40997  hdmapoc  41105  hlhilocv  41135  wepwsolem  42086  fnwe2lem2  42095  islnm2  42122  onmaxnelsup  42274  onsupnmax  42279  onsupuni  42280  onsupmaxb  42290  onsupeqnmax  42298  iscard5  42589  alephiso2  42611  clsk3nimkb  43093  ntrclsneine0  43118  ntrneineine0  43140  ntrneineine1  43141  ntrneicls00  43142  ntrneicls11  43143  ntrneiiso  43144  ntrneik2  43145  ntrneix2  43146  ntrneikb  43147  ntrneixb  43148  ntrneik3  43149  ntrneix3  43150  ntrneik13  43151  ntrneix13  43152  ntrneik4w  43153  ntrneik4  43154  caofcan  43384  infxrbnd2  44377  supminfxr  44472  rexanuz2nf  44501  evthiccabs  44507  ellimcabssub0  44631  climf  44636  clim2f  44650  clim2cf  44664  clim0cf  44668  limsupmnflem  44734  limsupre2lem  44738  limsupreuzmpt  44753  supcnvlimsup  44754  limsupge  44775  liminfreuzlem  44816  liminfltlem  44818  liminflimsupclim  44821  liminfpnfuz  44830  xlimpnfxnegmnf2  44872  fourierdlem70  45190  fourierdlem71  45191  fourierdlem73  45193  fourierdlem80  45200  fourierdlem83  45203  fourierdlem87  45207  voliunsge0lem  45486  meaiuninclem  45494  meaiuninc3v  45498  hoidmv1lelem3  45607  hoidmvlelem4  45612  hoidmvlelem5  45613  issmflem  45741  cfsetsnfsetf  46066  cfsetsnfsetfo  46068  requad2  46589  islinindfis  47217  elbigolo1  47330  line2x  47527  itscnhlinecirc02p  47558  iscnrm3lem1  47653  ipolublem  47698  ipoglblem  47701  aacllem  47935