Theorem ralbidva 3182

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  ralbidv  3184  2ralbidva  3225  raleqbidva  3340  poinxp  5780  soinxp  5781  frinxp  5782  ordunisssuc  6501  fnmptfvd  7074  funimass3  7087  fnnfpeq0  7212  cocan1  7327  cocan2  7328  isores2  7369  isoini2  7375  ofrfvalg  7722  ofrfval2  7735  tfindsg2  7899  f1oweALT  8013  fnsuppres  8232  dfsmo2  8403  smores  8408  smores2  8410  dfrecs3  8428  dfrecs3OLD  8429  naddunif  8749  ac6sfi  9348  fimaxg  9351  ordunifi  9354  isfinite2  9362  fipreima  9428  supisolem  9542  fiming  9567  infempty  9576  ordiso2  9584  ordtypelem7  9593  cantnf  9762  wemapwe  9766  rankval3b  9895  rankonidlem  9897  iscard  10044  acndom  10120  dfac12lem3  10215  kmlem2  10221  cflim2  10332  cfsmolem  10339  ttukeylem6  10583  alephreg  10651  suplem2pr  11122  axsup  11365  sup3  12252  infm3  12254  suprleub  12261  dfinfre  12276  infregelb  12279  ofsubeq0  12290  ofsubge0  12292  zextlt  12717  prime  12724  suprfinzcl  12757  indstr  12981  supxr2  13376  supxrbnd1  13383  supxrbnd2  13384  supxrleub  13388  supxrbnd  13390  infxrgelb  13397  fzshftral  13672  mptnn0fsupp  14048  swrdspsleq  14713  pfxeq  14744  clim  15540  rlim  15541  clim2  15550  clim2c  15551  clim0c  15553  ello1mpt  15567  lo1o1  15578  o1lo1  15583  climabs0  15631  o1compt  15633  rlimdiv  15694  geomulcvg  15924  mertenslem2  15933  mertens  15934  rpnnen2lem12  16273  sqrt2irr  16297  fprodfvdvdsd  16382  fproddvdsd  16383  dfgcd2  16593  isprm7  16755  pc11  16927  pcz  16928  1arith  16974  vdwlem8  17035  vdwlem11  17038  vdw  17041  ramval  17055  pwsle  17552  mrieqvd  17696  mreacs  17716  cidpropd  17768  ismon2  17795  monpropd  17798  isepi  17801  isepi2  17802  subsubc  17917  funcres2b  17961  funcpropd  17967  isfull2  17978  isfth2  17982  fucsect  18042  fucinv  18043  pospropd  18397  ipodrsfi  18609  tsrss  18659  grpidpropd  18700  sgrppropd  18769  mndpropd  18797  smndex1mnd  18945  grppropd  18991  issubg4  19185  gass  19341  gsmsymgrfixlem1  19469  gsmsymgreqlem2  19473  gexdvds  19626  gexdvds2  19627  subgpgp  19639  sylow3lem6  19674  efgval2  19766  efgsp1  19779  dprdf11  20067  subgdmdprd  20078  rngpropd  20201  ringpropd  20311  abvpropd  20858  lsspropd  21039  lbspropd  21121  isridlrng  21252  isridl  21285  phlpropd  21696  ishil2  21762  frlmplusgvalb  21812  frlmvscavalb  21813  frlmvplusgscavalb  21814  lindfmm  21870  islindf4  21881  islindf5  21882  assapropd  21915  psrbaglefi  21969  psrbagconf1o  21972  gsumbagdiaglem  21973  mplmonmul  22077  gsumply1eq  22334  scmatf1  22558  cpmatmcllem  22745  cpmatmcl  22746  decpmataa0  22795  decpmatmulsumfsupp  22800  pmatcollpw2lem  22804  pm2mpmhmlem1  22845  tgss2  23015  isclo  23116  neips  23142  opnnei  23149  isperf3  23182  ssidcn  23284  lmbrf  23289  cnnei  23311  cnrest2  23315  lmss  23327  lmres  23329  ist1-2  23376  ist1-3  23378  isreg2  23406  cmpfi  23437  bwth  23439  1stccn  23492  subislly  23510  kgencn  23585  ptclsg  23644  ptcnplem  23650  xkococnlem  23688  xkoinjcn  23716  tgqtop  23741  qtopcn  23743  fbflim  24005  flimrest  24012  flfnei  24020  isflf  24022  cnflf  24031  fclsopn  24043  fclsbas  24050  fclsrest  24053  isfcf  24063  cnfcf  24071  ptcmplem3  24083  tmdgsum2  24125  eltsms  24162  tsmsgsum  24168  tsmssubm  24172  tsmsf1o  24174  utopsnneiplem  24277  ismet2  24364  prdsxmetlem  24399  elmopn2  24476  prdsbl  24525  metss  24542  metrest  24558  metcnp  24575  metcnp2  24576  metcn  24577  metucn  24605  nrginvrcn  24734  metdsge  24890  divcnOLD  24909  divcn  24911  elcncf2  24935  mulc1cncf  24950  cncfmet  24954  evth2  25011  lmmbr2  25312  lmmbrf  25315  iscfil2  25319  cfil3i  25322  iscau2  25330  iscau4  25332  iscauf  25333  caucfil  25336  iscmet3lem3  25343  cfilres  25349  causs  25351  lmclim  25356  rrxmet  25461  evthicc2  25514  cniccbdd  25515  ovolfioo  25521  ovolficc  25522  ismbl2  25581  mbfsup  25718  mbfinf  25719  mbflimsup  25720  0plef  25726  mbfi1flim  25778  xrge0f  25786  itg2mulclem  25801  itgeqa  25869  ellimc2  25932  ellimc3  25934  limcflf  25936  cnlimc  25943  dvferm1  26043  dvferm2  26045  rolle  26048  dvivthlem1  26067  ftc1lem6  26102  itgsubst  26110  mdegle0  26136  deg1leb  26154  plydivex  26357  ulm2  26446  ulmcaulem  26455  ulmcau  26456  ulmdvlem3  26463  abelthlem9  26502  abelth  26503  rlimcnp  27026  ftalem3  27136  issqf  27197  sqf11  27200  mpodvdsmulf1o  27255  dvdsmulf1o  27257  dchrelbas4  27305  dchrinv  27323  2sqlem6  27485  chpo1ubb  27543  dchrmusumlema  27555  dchrisum0lema  27576  ostth3  27700  sltrec  27883  lrrecfr  27994  addsuniflem  28052  addsbday  28068  negsunif  28105  tgcgr4  28557  eqeelen  28937  brbtwn2  28938  colinearalg  28943  axcgrid  28949  axsegconlem1  28950  ax5seglem4  28965  ax5seglem5  28966  axbtwnid  28972  axpasch  28974  axeuclidlem  28995  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem12  29008  elntg2  29018  isuvtx  29430  uvtx2vtx1edg  29433  uvtx2vtx1edgb  29434  iscplgrnb  29451  iscplgredg  29452  vdiscusgrb  29566  uhgrvd00  29570  upgriswlk  29677  wwlksnext  29926  clwwlkinwwlk  30072  clwwlkel  30078  clwwlkf  30079  clwwlkwwlksb  30086  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  clwwlknonex2lem2  30140  nmounbi  30808  blocnilem  30836  isph  30854  phoeqi  30889  h2hcau  31011  h2hlm  31012  hial2eq2  31139  hoeq1  31862  hoeq2  31863  adjsym  31865  cnvadj  31924  hhcno  31936  hhcnf  31937  adjvalval  31969  leop2  32156  leoptri  32168  mdbr2  32328  dmdbr2  32335  mddmd2  32341  cdj3lem3b  32472  infxrge0gelb  32773  toslublem  32945  tosglblem  32947  mgccnv  32972  submarchi  33166  isarchi3  33167  lindfpropd  33375  opprlidlabs  33478  ply1moneq  33576  cmpcref  33796  lmdvg  33899  prodindf  33987  eulerpartlemd  34331  subfacp1lem3  35150  subfacp1lem5  35152  satfv1lem  35330  dfrdg2  35759  opnrebl  36286  poimirlem23  37603  broucube  37614  itg2gt0cn  37635  ftc1cnnc  37652  lmclim2  37718  caures  37720  sstotbnd2  37734  rrnmet  37789  rrncmslem  37792  isdrngo3  37919  isidlc  37975  cvrval2  39230  isat3  39263  iscvlat2N  39280  glbconN  39333  glbconNOLD  39334  ltrneq  40106  cdlemefrs29clN  40356  cdlemefrs32fva  40357  cdleme32fva  40394  cdlemk33N  40866  cdlemk34  40867  cdlemkid3N  40890  cdlemkid4  40891  diaglbN  41012  dibglbN  41123  dihglbcpreN  41257  dihglblem6  41297  hdmap1eulem  41779  hdmap1eulemOLDN  41780  hdmapoc  41888  hlhilocv  41918  primrootsunit1  42054  sn-sup3d  42448  fimgmcyc  42489  wepwsolem  42999  fnwe2lem2  43008  islnm2  43035  onmaxnelsup  43184  onsupnmax  43189  onsupuni  43190  onsupmaxb  43200  onsupeqnmax  43208  iscard5  43498  alephiso2  43520  clsk3nimkb  44002  ntrclsneine0  44027  ntrneineine0  44049  ntrneineine1  44050  ntrneicls00  44051  ntrneicls11  44052  ntrneiiso  44053  ntrneik2  44054  ntrneix2  44055  ntrneikb  44056  ntrneixb  44057  ntrneik3  44058  ntrneix3  44059  ntrneik13  44060  ntrneix13  44061  ntrneik4w  44062  ntrneik4  44063  caofcan  44292  infxrbnd2  45284  supminfxr  45379  rexanuz2nf  45408  evthiccabs  45414  ellimcabssub0  45538  climf  45543  clim2f  45557  clim2cf  45571  clim0cf  45575  limsupmnflem  45641  limsupre2lem  45645  limsupreuzmpt  45660  supcnvlimsup  45661  limsupge  45682  liminfreuzlem  45723  liminfltlem  45725  liminflimsupclim  45728  liminfpnfuz  45737  xlimpnfxnegmnf2  45779  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem80  46107  fourierdlem83  46110  fourierdlem87  46114  voliunsge0lem  46393  meaiuninclem  46401  meaiuninc3v  46405  hoidmv1lelem3  46514  hoidmvlelem4  46519  hoidmvlelem5  46520  issmflem  46648  cfsetsnfsetf  46973  cfsetsnfsetfo  46975  requad2  47497  isubgrgrim  47781  grlicref  47829  islinindfis  48178  elbigolo1  48291  line2x  48488  itscnhlinecirc02p  48519  iscnrm3lem1  48613  ipolublem  48658  ipoglblem  48661  aacllem  48895