Theorem ralbidva 3176

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ∀wral 3061

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 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3062

This theorem is referenced by:  ralbidv  3178  2ralbidva  3219  raleqbidva  3332  poinxp  5766  soinxp  5767  frinxp  5768  ordunisssuc  6490  fnmptfvd  7061  funimass3  7074  fnnfpeq0  7198  cocan1  7311  cocan2  7312  isores2  7353  isoini2  7359  ofrfvalg  7705  ofrfval2  7718  caofidlcan  7735  tfindsg2  7883  f1oweALT  7997  fnsuppres  8216  dfsmo2  8387  smores  8392  smores2  8394  dfrecs3  8412  dfrecs3OLD  8413  naddunif  8731  ac6sfi  9320  fimaxg  9323  ordunifi  9326  isfinite2  9334  fipreima  9398  supisolem  9513  fiming  9538  infempty  9547  ordiso2  9555  ordtypelem7  9564  cantnf  9733  wemapwe  9737  rankval3b  9866  rankonidlem  9868  iscard  10015  acndom  10091  dfac12lem3  10186  kmlem2  10192  cflim2  10303  cfsmolem  10310  ttukeylem6  10554  alephreg  10622  suplem2pr  11093  axsup  11336  sup3  12225  infm3  12227  suprleub  12234  dfinfre  12249  infregelb  12252  ofsubeq0  12263  ofsubge0  12265  zextlt  12692  prime  12699  suprfinzcl  12732  indstr  12958  supxr2  13356  supxrbnd1  13363  supxrbnd2  13364  supxrleub  13368  supxrbnd  13370  infxrgelb  13377  fzshftral  13655  mptnn0fsupp  14038  swrdspsleq  14703  pfxeq  14734  clim  15530  rlim  15531  clim2  15540  clim2c  15541  clim0c  15543  ello1mpt  15557  lo1o1  15568  o1lo1  15573  climabs0  15621  o1compt  15623  rlimdiv  15682  geomulcvg  15912  mertenslem2  15921  mertens  15922  rpnnen2lem12  16261  sqrt2irr  16285  fprodfvdvdsd  16371  fproddvdsd  16372  dfgcd2  16583  isprm7  16745  pc11  16918  pcz  16919  1arith  16965  vdwlem8  17026  vdwlem11  17029  vdw  17032  ramval  17046  pwsle  17537  mrieqvd  17681  mreacs  17701  cidpropd  17753  ismon2  17778  monpropd  17781  isepi  17784  isepi2  17785  subsubc  17898  funcres2b  17942  funcpropd  17947  isfull2  17958  isfth2  17962  fucsect  18020  fucinv  18021  pospropd  18372  ipodrsfi  18584  tsrss  18634  grpidpropd  18675  sgrppropd  18744  mndpropd  18772  smndex1mnd  18923  grppropd  18969  issubg4  19163  gass  19319  gsmsymgrfixlem1  19445  gsmsymgreqlem2  19449  gexdvds  19602  gexdvds2  19603  subgpgp  19615  sylow3lem6  19650  efgval2  19742  efgsp1  19755  dprdf11  20043  subgdmdprd  20054  rngpropd  20171  ringpropd  20285  abvpropd  20836  lsspropd  21016  lbspropd  21098  isridlrng  21229  isridl  21262  phlpropd  21673  ishil2  21739  frlmplusgvalb  21789  frlmvscavalb  21790  frlmvplusgscavalb  21791  lindfmm  21847  islindf4  21858  islindf5  21859  assapropd  21892  psrbaglefi  21946  psrbagconf1o  21949  gsumbagdiaglem  21950  mplmonmul  22054  gsumply1eq  22313  scmatf1  22537  cpmatmcllem  22724  cpmatmcl  22725  decpmataa0  22774  decpmatmulsumfsupp  22779  pmatcollpw2lem  22783  pm2mpmhmlem1  22824  tgss2  22994  isclo  23095  neips  23121  opnnei  23128  isperf3  23161  ssidcn  23263  lmbrf  23268  cnnei  23290  cnrest2  23294  lmss  23306  lmres  23308  ist1-2  23355  ist1-3  23357  isreg2  23385  cmpfi  23416  bwth  23418  1stccn  23471  subislly  23489  kgencn  23564  ptclsg  23623  ptcnplem  23629  xkococnlem  23667  xkoinjcn  23695  tgqtop  23720  qtopcn  23722  fbflim  23984  flimrest  23991  flfnei  23999  isflf  24001  cnflf  24010  fclsopn  24022  fclsbas  24029  fclsrest  24032  isfcf  24042  cnfcf  24050  ptcmplem3  24062  tmdgsum2  24104  eltsms  24141  tsmsgsum  24147  tsmssubm  24151  tsmsf1o  24153  utopsnneiplem  24256  ismet2  24343  prdsxmetlem  24378  elmopn2  24455  prdsbl  24504  metss  24521  metrest  24537  metcnp  24554  metcnp2  24555  metcn  24556  metucn  24584  nrginvrcn  24713  metdsge  24871  divcnOLD  24890  divcn  24892  elcncf2  24916  mulc1cncf  24931  cncfmet  24935  evth2  24992  lmmbr2  25293  lmmbrf  25296  iscfil2  25300  cfil3i  25303  iscau2  25311  iscau4  25313  iscauf  25314  caucfil  25317  iscmet3lem3  25324  cfilres  25330  causs  25332  lmclim  25337  rrxmet  25442  evthicc2  25495  cniccbdd  25496  ovolfioo  25502  ovolficc  25503  ismbl2  25562  mbfsup  25699  mbfinf  25700  mbflimsup  25701  0plef  25707  mbfi1flim  25758  xrge0f  25766  itg2mulclem  25781  itgeqa  25849  ellimc2  25912  ellimc3  25914  limcflf  25916  cnlimc  25923  dvferm1  26023  dvferm2  26025  rolle  26028  dvivthlem1  26047  ftc1lem6  26082  itgsubst  26090  mdegle0  26116  deg1leb  26134  plydivex  26339  ulm2  26428  ulmcaulem  26437  ulmcau  26438  ulmdvlem3  26445  abelthlem9  26484  abelth  26485  rlimcnp  27008  ftalem3  27118  issqf  27179  sqf11  27182  mpodvdsmulf1o  27237  dvdsmulf1o  27239  dchrelbas4  27287  dchrinv  27305  2sqlem6  27467  chpo1ubb  27525  dchrmusumlema  27537  dchrisum0lema  27558  ostth3  27682  sltrec  27865  lrrecfr  27976  addsuniflem  28034  addsbday  28050  negsunif  28087  tgcgr4  28539  eqeelen  28919  brbtwn2  28920  colinearalg  28925  axcgrid  28931  axsegconlem1  28932  ax5seglem4  28947  ax5seglem5  28948  axbtwnid  28954  axpasch  28956  axeuclidlem  28977  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  axcontlem12  28990  elntg2  29000  isuvtx  29412  uvtx2vtx1edg  29415  uvtx2vtx1edgb  29416  iscplgrnb  29433  iscplgredg  29434  vdiscusgrb  29548  uhgrvd00  29552  upgriswlk  29659  wwlksnext  29913  clwwlkinwwlk  30059  clwwlkel  30065  clwwlkf  30066  clwwlkwwlksb  30073  wwlksext2clwwlk  30076  wwlksubclwwlk  30077  clwwlknonex2lem2  30127  nmounbi  30795  blocnilem  30823  isph  30841  phoeqi  30876  h2hcau  30998  h2hlm  30999  hial2eq2  31126  hoeq1  31849  hoeq2  31850  adjsym  31852  cnvadj  31911  hhcno  31923  hhcnf  31924  adjvalval  31956  leop2  32143  leoptri  32155  mdbr2  32315  dmdbr2  32322  mddmd2  32328  cdj3lem3b  32459  infxrge0gelb  32770  prodindf  32848  toslublem  32962  tosglblem  32964  mgccnv  32989  submarchi  33193  isarchi3  33194  lindfpropd  33410  opprlidlabs  33513  ply1moneq  33611  cmpcref  33849  lmdvg  33952  eulerpartlemd  34368  subfacp1lem3  35187  subfacp1lem5  35189  satfv1lem  35367  dfrdg2  35796  opnrebl  36321  poimirlem23  37650  broucube  37661  itg2gt0cn  37682  ftc1cnnc  37699  lmclim2  37765  caures  37767  sstotbnd2  37781  rrnmet  37836  rrncmslem  37839  isdrngo3  37966  isidlc  38022  cvrval2  39275  isat3  39308  iscvlat2N  39325  glbconN  39378  glbconNOLD  39379  ltrneq  40151  cdlemefrs29clN  40401  cdlemefrs32fva  40402  cdleme32fva  40439  cdlemk33N  40911  cdlemk34  40912  cdlemkid3N  40935  cdlemkid4  40936  diaglbN  41057  dibglbN  41168  dihglbcpreN  41302  dihglblem6  41342  hdmap1eulem  41824  hdmap1eulemOLDN  41825  hdmapoc  41933  hlhilocv  41963  primrootsunit1  42098  sn-sup3d  42502  fimgmcyc  42544  wepwsolem  43054  fnwe2lem2  43063  islnm2  43090  onmaxnelsup  43235  onsupnmax  43240  onsupuni  43241  onsupmaxb  43251  onsupeqnmax  43259  iscard5  43549  alephiso2  43571  clsk3nimkb  44053  ntrclsneine0  44078  ntrneineine0  44100  ntrneineine1  44101  ntrneicls00  44102  ntrneicls11  44103  ntrneiiso  44104  ntrneik2  44105  ntrneix2  44106  ntrneikb  44107  ntrneixb  44108  ntrneik3  44109  ntrneix3  44110  ntrneik13  44111  ntrneix13  44112  ntrneik4w  44113  ntrneik4  44114  caofcan  44342  modelac8prim  45009  infxrbnd2  45380  supminfxr  45475  rexanuz2nf  45503  evthiccabs  45509  ellimcabssub0  45632  climf  45637  clim2f  45651  clim2cf  45665  clim0cf  45669  limsupmnflem  45735  limsupre2lem  45739  limsupreuzmpt  45754  supcnvlimsup  45755  limsupge  45776  liminfreuzlem  45817  liminfltlem  45819  liminflimsupclim  45822  liminfpnfuz  45831  xlimpnfxnegmnf2  45873  fourierdlem70  46191  fourierdlem71  46192  fourierdlem73  46194  fourierdlem80  46201  fourierdlem83  46204  fourierdlem87  46208  voliunsge0lem  46487  meaiuninclem  46495  meaiuninc3v  46499  hoidmv1lelem3  46608  hoidmvlelem4  46613  hoidmvlelem5  46614  issmflem  46742  cfsetsnfsetf  47070  cfsetsnfsetfo  47072  requad2  47610  isubgrgrim  47897  grlicref  47972  islinindfis  48366  elbigolo1  48478  line2x  48675  itscnhlinecirc02p  48706  iscnrm3lem1  48831  ipolublem  48875  ipoglblem  48878  oppcup  48948  termc2  49148  aacllem  49320