Theorem ralbidva 3185

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3079

This theorem is used by:  ralbidv  3187  2ralbidva  3226  raleqbidva  3327  poinxp  5740  soinxp  5741  frinxp  5742  ordunisssuc  6470  fnmptfvd  7037  funimass3  7050  fnnfpeq0  7179  cocan1  7295  cocan2  7296  isores2  7337  isoini2  7343  ofrfvalg  7689  ofrfval2  7702  caofidlcan  7719  tfindsg2  7861  f1oweALT  7972  fnsuppres  8192  dfsmo2  8339  smores  8344  smores2  8346  dfrecs3  8364  naddunif  8685  ac6sfi  9257  fimaxg  9260  ordunifi  9263  isfinite2  9271  fipreima  9328  supisolem  9447  fiming  9473  infempty  9482  ordiso2  9490  ordtypelem7  9499  cantnf  9675  wemapwe  9679  rankval3b  9811  rankonidlem  9813  iscard  9983  acndom  10057  dfac12lem3  10151  kmlem2  10157  cflim2  10268  cfsmolem  10275  ttukeylem6  10519  alephreg  10594  suplem2pr  11065  axsup  11312  sup3  12199  infm3  12201  suprleub  12208  dfinfre  12223  infregelb  12226  ofsubeq0  12242  ofsubge0  12244  zextlt  12698  prime  12705  suprfinzcl  12738  indstr  12968  supxr2  13368  supxrbnd1  13375  supxrbnd2  13376  supxrleub  13380  supxrbnd  13382  infxrgelb  13390  fzshftral  13672  mptnn0fsupp  14063  swrdspsleq  14737  pfxeq  14767  clim  15583  rlim  15584  clim2  15593  clim2c  15594  clim0c  15596  ello1mpt  15610  lo1o1  15621  o1lo1  15626  climabs0  15674  o1compt  15676  rlimdiv  15735  geomulcvg  15967  mertenslem2  15976  mertens  15977  rpnnen2lem12  16317  sqrt2irr  16341  fprodfvdvdsd  16428  fproddvdsd  16429  dfgcd2  16640  isprm7  16803  pc11  16976  pcz  16977  1arith  17023  vdwlem8  17084  vdwlem11  17087  vdw  17090  ramval  17104  pwsle  17582  mrieqvd  17730  mreacs  17750  cidpropd  17802  ismon2  17827  monpropd  17830  isepi  17833  isepi2  17834  subsubc  17946  funcres2b  17990  funcpropd  17995  isfull2  18006  isfth2  18010  fucsect  18068  fucinv  18069  pospropd  18417  ipodrsfi  18631  tsrss  18681  grpidpropd  18759  mgmidpfod  18774  sgrppropd  18835  mndpropd  18866  smndex1mnd  19023  grppropd  19076  issubg4  19270  gass  19429  gsmsymgrfixlem1  19555  gsmsymgreqlem2  19559  gexdvds  19712  gexdvds2  19713  subgpgp  19725  sylow3lem6  19760  efgval2  19852  efgsp1  19865  dprdf11  20153  subgdmdprd  20164  rngpropd  20310  ringpropd  20431  isdrng5  20918  abvpropd  21002  lsspropd  21202  lbspropd  21284  isridlrng  21408  isridl  21455  phlpropd  21869  ishil2  21933  frlmplusgvalb  21983  frlmvscavalb  21984  frlmvplusgscavalb  21985  lindfmm  22041  islindf4  22052  islindf5  22053  assapropd  22087  psrbaglefi  22142  psrbagconf1o  22145  gsumbagdiaglem  22147  mplmonmul  22253  gsumply1eq  22535  scmatf1  22754  cpmatmcllem  22944  cpmatmcl  22945  decpmataa0  22994  decpmatmulsumfsupp  22999  pmatcollpw2lem  23003  pm2mpmhmlem1  23044  tgss2  23213  isclo  23313  neips  23339  opnnei  23346  isperf3  23379  ssidcn  23481  lmbrf  23486  cnnei  23508  cnrest2  23512  lmss  23524  lmres  23526  ist1-2  23573  ist1-3  23575  isreg2  23603  cmpfi  23634  bwth  23636  1stccn  23690  subislly  23708  kgencn  23783  ptclsg  23842  ptcnplem  23848  xkococnlem  23886  xkoinjcn  23914  tgqtop  23939  qtopcn  23941  fbflim  24203  flimrest  24210  flfnei  24218  isflf  24220  cnflf  24229  fclsopn  24241  fclsbas  24248  fclsrest  24251  isfcf  24261  cnfcf  24269  ptcmplem3  24281  tmdgsum2  24323  eltsms  24360  tsmsgsum  24366  tsmssubm  24370  tsmsf1o  24372  utopsnneiplem  24474  ismet2  24560  prdsxmetlem  24595  elmopn2  24672  prdsbl  24718  metss  24735  metrest  24751  metcnp  24768  metcnp2  24769  metcn  24770  metucn  24798  nrginvrcn  24919  metdsge  25077  divcn  25097  elcncf2  25119  mulc1cncf  25134  cncfmet  25138  evth2  25189  lmmbr2  25488  lmmbrf  25491  iscfil2  25495  cfil3i  25498  iscau2  25506  iscau4  25508  iscauf  25509  caucfil  25512  iscmet3lem3  25519  cfilres  25525  causs  25527  lmclim  25532  rrxmet  25637  evthicc2  25689  cniccbdd  25690  ovolfioo  25696  ovolficc  25697  ismbl2  25756  mbfsup  25893  mbfinf  25894  mbflimsup  25895  0plef  25901  mbfi1flim  25952  xrge0f  25960  itg2mulclem  25975  itgeqa  26043  ellimc2  26106  ellimc3  26108  limcflf  26110  cnlimc  26117  dvferm1  26214  dvferm2  26216  rolle  26219  dvivthlem1  26237  ftc1lem6  26270  itgsubst  26278  mdegle0  26304  deg1leb  26322  plydivex  26528  ulm2  26618  ulmcaulem  26627  ulmcau  26628  ulmdvlem3  26635  abelthlem9  26673  abelth  26674  rlimcnp  27200  ftalem3  27309  issqf  27370  sqf11  27373  mpodvdsmulf1o  27428  dvdsmulf1o  27430  dchrelbas4  27477  dchrinv  27495  2sqlem6  27657  chpo1ubb  27715  dchrmusumlema  27727  dchrisum0lema  27748  ostth3  27872  ltsrec  28064  lrrecfr  28206  addsuniflem  28264  addbday  28281  negsunif  28318  n0fincut  28618  bdayfinbndlem1  28730  elreno2  28758  tgcgr4  28871  eqeelen  29347  brbtwn2  29348  colinearalg  29353  axcgrid  29359  axsegconlem1  29360  ax5seglem4  29375  ax5seglem5  29376  axbtwnid  29382  axpasch  29384  axeuclidlem  29405  axcontlem2  29408  axcontlem4  29410  axcontlem7  29413  axcontlem12  29418  elntg2  29428  isuvtx  29841  uvtx2vtx1edg  29844  uvtx2vtx1edgb  29845  iscplgrnb  29862  iscplgredg  29863  vdiscusgrb  29976  uhgrvd00  29980  upgriswlk  30086  wwlksnext  30347  clwwlkinwwlk  30496  clwwlkel  30502  clwwlkf  30503  clwwlkwwlksb  30510  wwlksext2clwwlk  30513  wwlksubclwwlk  30514  clwwlknonex2lem2  30564  nmounbi  31243  blocnilem  31271  isph  31289  phoeqi  31324  h2hcau  31446  h2hlm  31447  hial2eq2  31574  hoeq1  32297  hoeq2  32298  adjsym  32300  cnvadj  32359  hhcno  32371  hhcnf  32372  adjvalval  32404  leop2  32591  leoptri  32603  mdbr2  32763  dmdbr2  32770  mddmd2  32776  cdj3lem3b  32907  infxrge0gelb  33224  prodindf  33295  toslublem  33399  tosglblem  33401  mgccnv  33426  cntrval2  33598  submarchi  33613  isarchi3  33614  lindfpropd  33802  opprlidlabs  33874  ply1moneq  33985  psrmonmul  34047  cmpcref  34347  lmdvg  34450  eulerpartlemd  34864  subfacp1lem3  35748  subfacp1lem5  35750  satfv1lem  35928  dfrdg2  36359  nadddilem2  36788  nadddilem4  36790  opnrebl  36926  poimirlem23  38379  broucube  38390  itg2gt0cn  38411  ftc1cnnc  38428  lmclim2  38495  caures  38497  sstotbnd2  38511  rrnmet  38566  rrncmslem  38569  isdrngo3  38696  isidlc  38752  cvrval2  40134  isat3  40167  iscvlat2N  40184  glbconN  40237  ltrneq  41009  cdlemefrs29clN  41259  cdlemefrs32fva  41260  cdleme32fva  41297  cdlemk33N  41769  cdlemk34  41770  cdlemkid3N  41793  cdlemkid4  41794  diaglbN  41915  dibglbN  42026  dihglbcpreN  42160  dihglblem6  42200  hdmap1eulem  42682  hdmap1eulemOLDN  42683  hdmapoc  42791  hlhilocv  42817  primrootsunit1  42950  sn-sup3d  43367  fimgmcyc  43403  wepwsolem  43870  fnwe2lem2  43879  islnm2  43906  onmaxnelsup  44051  onsupnmax  44056  onsupuni  44057  onsupmaxb  44067  onsupeqnmax  44075  iscard5  44363  alephiso2  44385  clsk3nimkb  44867  ntrclsneine0  44892  ntrneineine0  44914  ntrneineine1  44915  ntrneicls00  44916  ntrneicls11  44917  ntrneiiso  44918  ntrneik2  44919  ntrneix2  44920  ntrneikb  44921  ntrneixb  44922  ntrneik3  44923  ntrneix3  44924  ntrneik13  44925  ntrneix13  44926  ntrneik4w  44927  ntrneik4  44928  caofcan  45134  modelac8prim  45802  infxrbnd2  46185  supminfxr  46279  rexanuz2nf  46307  evthiccabs  46313  ellimcabssub0  46434  climf  46439  clim2f  46451  clim2cf  46465  clim0cf  46469  limsupmnflem  46535  limsupre2lem  46539  limsupreuzmpt  46554  supcnvlimsup  46555  limsupge  46576  liminfreuzlem  46617  liminfltlem  46619  liminflimsupclim  46622  liminfpnfuz  46631  xlimpnfxnegmnf2  46673  fourierdlem70  46991  fourierdlem71  46992  fourierdlem73  46994  fourierdlem80  47001  fourierdlem83  47004  fourierdlem87  47008  voliunsge0lem  47287  meaiuninclem  47295  meaiuninc3v  47299  hoidmv1lelem3  47408  hoidmvlelem4  47413  hoidmvlelem5  47414  issmflem  47542  chnerlem1  47697  cfsetsnfsetf  47933  cfsetsnfsetfo  47935  nprmmul1  48414  requad2  48526  isubgrgrim  48832  grlicref  48915  islinindfis  49366  elbigolo1  49474  line2x  49671  itscnhlinecirc02p  49702  iscnrm3lem1  49847  ipolublem  49899  ipoglblem  49902  oppcup  50120  uptrlem3  50125  initopropd  50156  termopropd  50157  isinito2lem  50411  termc2  50431  lanup  50554  ranup  50555  aacllem  50759