Theorem ralbidva 3175

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 3173	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

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

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 3062

This theorem is referenced by:  ralbidv  3177  2ralbidva  3216  raleqbidva  3327  poinxp  5756  soinxp  5757  frinxp  5758  ordunisssuc  6470  fnmptfvd  7042  funimass3  7055  fnnfpeq0  7175  cocan1  7288  cocan2  7289  isores2  7329  isoini2  7335  ofrfvalg  7677  ofrfval2  7690  tfindsg2  7850  f1oweALT  7958  fnsuppres  8175  dfsmo2  8346  smores  8351  smores2  8353  dfrecs3  8371  dfrecs3OLD  8372  naddunif  8691  ac6sfi  9286  fimaxg  9289  ordunifi  9292  isfinite2  9300  fipreima  9357  supisolem  9467  fiming  9492  infempty  9501  ordiso2  9509  ordtypelem7  9518  cantnf  9687  wemapwe  9691  rankval3b  9820  rankonidlem  9822  iscard  9969  acndom  10045  dfac12lem3  10139  kmlem2  10145  cflim2  10257  cfsmolem  10264  ttukeylem6  10508  alephreg  10576  suplem2pr  11047  axsup  11288  sup3  12170  infm3  12172  suprleub  12179  dfinfre  12194  infregelb  12197  ofsubeq0  12208  ofsubge0  12210  zextlt  12635  prime  12642  suprfinzcl  12675  indstr  12899  supxr2  13292  supxrbnd1  13299  supxrbnd2  13300  supxrleub  13304  supxrbnd  13306  infxrgelb  13313  fzshftral  13588  mptnn0fsupp  13961  swrdspsleq  14614  pfxeq  14645  clim  15437  rlim  15438  clim2  15447  clim2c  15448  clim0c  15450  ello1mpt  15464  lo1o1  15475  o1lo1  15480  climabs0  15528  o1compt  15530  rlimdiv  15591  geomulcvg  15821  mertenslem2  15830  mertens  15831  rpnnen2lem12  16167  sqrt2irr  16191  fprodfvdvdsd  16276  fproddvdsd  16277  dfgcd2  16487  isprm7  16644  pc11  16812  pcz  16813  1arith  16859  vdwlem8  16920  vdwlem11  16923  vdw  16926  ramval  16940  pwsle  17437  mrieqvd  17581  mreacs  17601  cidpropd  17653  ismon2  17680  monpropd  17683  isepi  17686  isepi2  17687  subsubc  17802  funcres2b  17846  funcpropd  17850  isfull2  17861  isfth2  17865  fucsect  17924  fucinv  17925  pospropd  18279  ipodrsfi  18491  tsrss  18541  grpidpropd  18580  sgrppropd  18621  mndpropd  18649  smndex1mnd  18790  grppropd  18836  issubg4  19024  gass  19164  gsmsymgrfixlem1  19294  gsmsymgreqlem2  19298  gexdvds  19451  gexdvds2  19452  subgpgp  19464  sylow3lem6  19499  efgval2  19591  efgsp1  19604  dprdf11  19892  subgdmdprd  19903  ringpropd  20101  abvpropd  20449  lsspropd  20627  lbspropd  20709  isridl  20858  phlpropd  21207  ishil2  21273  frlmplusgvalb  21323  frlmvscavalb  21324  frlmvplusgscavalb  21325  lindfmm  21381  islindf4  21392  islindf5  21393  assapropd  21425  psrbaglefi  21484  psrbaglefiOLD  21485  psrbagconf1o  21488  psrbagconf1oOLD  21489  gsumbagdiaglemOLD  21490  gsumbagdiaglem  21493  mplmonmul  21590  gsumply1eq  21828  scmatf1  22032  cpmatmcllem  22219  cpmatmcl  22220  decpmataa0  22269  decpmatmulsumfsupp  22274  pmatcollpw2lem  22278  pm2mpmhmlem1  22319  tgss2  22489  isclo  22590  neips  22616  opnnei  22623  isperf3  22656  ssidcn  22758  lmbrf  22763  cnnei  22785  cnrest2  22789  lmss  22801  lmres  22803  ist1-2  22850  ist1-3  22852  isreg2  22880  cmpfi  22911  bwth  22913  1stccn  22966  subislly  22984  kgencn  23059  ptclsg  23118  ptcnplem  23124  xkococnlem  23162  xkoinjcn  23190  tgqtop  23215  qtopcn  23217  fbflim  23479  flimrest  23486  flfnei  23494  isflf  23496  cnflf  23505  fclsopn  23517  fclsbas  23524  fclsrest  23527  isfcf  23537  cnfcf  23545  ptcmplem3  23557  tmdgsum2  23599  eltsms  23636  tsmsgsum  23642  tsmssubm  23646  tsmsf1o  23648  utopsnneiplem  23751  ismet2  23838  prdsxmetlem  23873  elmopn2  23950  prdsbl  23999  metss  24016  metrest  24032  metcnp  24049  metcnp2  24050  metcn  24051  metucn  24079  nrginvrcn  24208  metdsge  24364  divcn  24383  elcncf2  24405  mulc1cncf  24420  cncfmet  24424  evth2  24475  lmmbr2  24775  lmmbrf  24778  iscfil2  24782  cfil3i  24785  iscau2  24793  iscau4  24795  iscauf  24796  caucfil  24799  iscmet3lem3  24806  cfilres  24812  causs  24814  lmclim  24819  rrxmet  24924  evthicc2  24976  cniccbdd  24977  ovolfioo  24983  ovolficc  24984  ismbl2  25043  mbfsup  25180  mbfinf  25181  mbflimsup  25182  0plef  25188  mbfi1flim  25240  xrge0f  25248  itg2mulclem  25263  itgeqa  25330  ellimc2  25393  ellimc3  25395  limcflf  25397  cnlimc  25404  dvferm1  25501  dvferm2  25503  rolle  25506  dvivthlem1  25524  ftc1lem6  25557  itgsubst  25565  mdegle0  25594  deg1leb  25612  plydivex  25809  ulm2  25896  ulmcaulem  25905  ulmcau  25906  ulmdvlem3  25913  abelthlem9  25951  abelth  25952  rlimcnp  26467  ftalem3  26576  issqf  26637  sqf11  26640  dvdsmulf1o  26695  dchrelbas4  26743  dchrinv  26761  2sqlem6  26923  chpo1ubb  26981  dchrmusumlema  26993  dchrisum0lema  27014  ostth3  27138  sltrec  27318  lrrecfr  27424  addsuniflem  27481  negsunif  27526  tgcgr4  27779  eqeelen  28159  brbtwn2  28160  colinearalg  28165  axcgrid  28171  axsegconlem1  28172  ax5seglem4  28187  ax5seglem5  28188  axbtwnid  28194  axpasch  28196  axeuclidlem  28217  axcontlem2  28220  axcontlem4  28222  axcontlem7  28225  axcontlem12  28230  elntg2  28240  isuvtx  28649  uvtx2vtx1edg  28652  uvtx2vtx1edgb  28653  iscplgrnb  28670  iscplgredg  28671  vdiscusgrb  28784  uhgrvd00  28788  upgriswlk  28895  wwlksnext  29144  clwwlkinwwlk  29290  clwwlkel  29296  clwwlkf  29297  clwwlkwwlksb  29304  wwlksext2clwwlk  29307  wwlksubclwwlk  29308  clwwlknonex2lem2  29358  nmounbi  30024  blocnilem  30052  isph  30070  phoeqi  30105  h2hcau  30227  h2hlm  30228  hial2eq2  30355  hoeq1  31078  hoeq2  31079  adjsym  31081  cnvadj  31140  hhcno  31152  hhcnf  31153  adjvalval  31185  leop2  31372  leoptri  31384  mdbr2  31544  dmdbr2  31551  mddmd2  31557  cdj3lem3b  31688  infxrge0gelb  31974  toslublem  32137  tosglblem  32139  mgccnv  32164  submarchi  32327  isarchi3  32328  lindfpropd  32493  opprlidlabs  32594  ply1moneq  32660  cmpcref  32825  lmdvg  32928  prodindf  33016  eulerpartlemd  33360  subfacp1lem3  34168  subfacp1lem5  34170  satfv1lem  34348  dfrdg2  34762  gg-divcn  35158  opnrebl  35200  poimirlem23  36506  broucube  36517  itg2gt0cn  36538  ftc1cnnc  36555  lmclim2  36621  caures  36623  sstotbnd2  36637  rrnmet  36692  rrncmslem  36695  isdrngo3  36822  isidlc  36878  cvrval2  38139  isat3  38172  iscvlat2N  38189  glbconN  38242  glbconNOLD  38243  ltrneq  39015  cdlemefrs29clN  39265  cdlemefrs32fva  39266  cdleme32fva  39303  cdlemk33N  39775  cdlemk34  39776  cdlemkid3N  39799  cdlemkid4  39800  diaglbN  39921  dibglbN  40032  dihglbcpreN  40166  dihglblem6  40206  hdmap1eulem  40688  hdmap1eulemOLDN  40689  hdmapoc  40797  hlhilocv  40827  wepwsolem  41774  fnwe2lem2  41783  islnm2  41810  onmaxnelsup  41962  onsupnmax  41967  onsupuni  41968  onsupmaxb  41978  onsupeqnmax  41986  iscard5  42277  alephiso2  42299  clsk3nimkb  42781  ntrclsneine0  42806  ntrneineine0  42828  ntrneineine1  42829  ntrneicls00  42830  ntrneicls11  42831  ntrneiiso  42832  ntrneik2  42833  ntrneix2  42834  ntrneikb  42835  ntrneixb  42836  ntrneik3  42837  ntrneix3  42838  ntrneik13  42839  ntrneix13  42840  ntrneik4w  42841  ntrneik4  42842  caofcan  43072  infxrbnd2  44069  supminfxr  44164  rexanuz2nf  44193  evthiccabs  44199  ellimcabssub0  44323  climf  44328  clim2f  44342  clim2cf  44356  clim0cf  44360  limsupmnflem  44426  limsupre2lem  44430  limsupreuzmpt  44445  supcnvlimsup  44446  limsupge  44467  liminfreuzlem  44508  liminfltlem  44510  liminflimsupclim  44513  liminfpnfuz  44522  xlimpnfxnegmnf2  44564  fourierdlem70  44882  fourierdlem71  44883  fourierdlem73  44885  fourierdlem80  44892  fourierdlem83  44895  fourierdlem87  44899  voliunsge0lem  45178  meaiuninclem  45186  meaiuninc3v  45190  hoidmv1lelem3  45299  hoidmvlelem4  45304  hoidmvlelem5  45305  issmflem  45433  cfsetsnfsetf  45758  cfsetsnfsetfo  45760  requad2  46281  rngpropd  46663  isridlrng  46741  islinindfis  47120  elbigolo1  47233  line2x  47430  itscnhlinecirc02p  47461  iscnrm3lem1  47556  ipolublem  47601  ipoglblem  47604  aacllem  47838