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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

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

This theorem is used by:  ralbidv  3187  2ralbidva  3226  raleqbidva  3328  poinxp  5741  soinxp  5742  frinxp  5743  ordunisssuc  6469  fnmptfvd  7036  funimass3  7049  fnnfpeq0  7176  cocan1  7289  cocan2  7290  isores2  7331  isoini2  7337  ofrfvalg  7684  ofrfval2  7697  caofidlcan  7714  tfindsg2  7856  f1oweALT  7967  fnsuppres  8185  dfsmo2  8332  smores  8337  smores2  8339  dfrecs3  8357  naddunif  8678  ac6sfi  9242  fimaxg  9245  ordunifi  9248  isfinite2  9256  fipreima  9313  supisolem  9432  fiming  9458  infempty  9467  ordiso2  9475  ordtypelem7  9484  cantnf  9660  wemapwe  9664  rankval3b  9796  rankonidlem  9798  iscard  9968  acndom  10042  dfac12lem3  10136  kmlem2  10142  cflim2  10253  cfsmolem  10260  ttukeylem6  10504  alephreg  10573  suplem2pr  11044  axsup  11291  sup3  12178  infm3  12180  suprleub  12187  dfinfre  12202  infregelb  12205  ofsubeq0  12221  ofsubge0  12223  zextlt  12676  prime  12683  suprfinzcl  12716  indstr  12946  supxr2  13346  supxrbnd1  13353  supxrbnd2  13354  supxrleub  13358  supxrbnd  13360  infxrgelb  13368  fzshftral  13650  mptnn0fsupp  14040  swrdspsleq  14710  pfxeq  14740  clim  15552  rlim  15553  clim2  15562  clim2c  15563  clim0c  15565  ello1mpt  15579  lo1o1  15590  o1lo1  15595  climabs0  15643  o1compt  15645  rlimdiv  15704  geomulcvg  15937  mertenslem2  15946  mertens  15947  rpnnen2lem12  16287  sqrt2irr  16311  fprodfvdvdsd  16398  fproddvdsd  16399  dfgcd2  16610  isprm7  16773  pc11  16946  pcz  16947  1arith  16993  vdwlem8  17054  vdwlem11  17057  vdw  17060  ramval  17074  pwsle  17552  mrieqvd  17700  mreacs  17720  cidpropd  17772  ismon2  17797  monpropd  17800  isepi  17803  isepi2  17804  subsubc  17916  funcres2b  17960  funcpropd  17965  isfull2  17976  isfth2  17980  fucsect  18038  fucinv  18039  pospropd  18387  ipodrsfi  18601  tsrss  18651  grpidpropd  18726  sgrppropd  18795  mndpropd  18823  smndex1mnd  18978  grppropd  19024  issubg4  19218  gass  19377  gsmsymgrfixlem1  19503  gsmsymgreqlem2  19507  gexdvds  19660  gexdvds2  19661  subgpgp  19673  sylow3lem6  19708  efgval2  19800  efgsp1  19813  dprdf11  20101  subgdmdprd  20112  rngpropd  20258  ringpropd  20378  isdrng5  20865  abvpropd  20949  lsspropd  21149  lbspropd  21231  isridlrng  21355  isridl  21402  phlpropd  21816  ishil2  21880  frlmplusgvalb  21930  frlmvscavalb  21931  frlmvplusgscavalb  21932  lindfmm  21988  islindf4  21999  islindf5  22000  assapropd  22032  psrbaglefi  22087  psrbagconf1o  22090  gsumbagdiaglem  22092  mplmonmul  22198  gsumply1eq  22480  scmatf1  22699  cpmatmcllem  22886  cpmatmcl  22887  decpmataa0  22936  decpmatmulsumfsupp  22941  pmatcollpw2lem  22945  pm2mpmhmlem1  22986  tgss2  23155  isclo  23255  neips  23281  opnnei  23288  isperf3  23321  ssidcn  23423  lmbrf  23428  cnnei  23450  cnrest2  23454  lmss  23466  lmres  23468  ist1-2  23515  ist1-3  23517  isreg2  23545  cmpfi  23576  bwth  23578  1stccn  23631  subislly  23649  kgencn  23724  ptclsg  23783  ptcnplem  23789  xkococnlem  23827  xkoinjcn  23855  tgqtop  23880  qtopcn  23882  fbflim  24144  flimrest  24151  flfnei  24159  isflf  24161  cnflf  24170  fclsopn  24182  fclsbas  24189  fclsrest  24192  isfcf  24202  cnfcf  24210  ptcmplem3  24222  tmdgsum2  24264  eltsms  24301  tsmsgsum  24307  tsmssubm  24311  tsmsf1o  24313  utopsnneiplem  24415  ismet2  24501  prdsxmetlem  24536  elmopn2  24613  prdsbl  24659  metss  24676  metrest  24692  metcnp  24709  metcnp2  24710  metcn  24711  metucn  24739  nrginvrcn  24860  metdsge  25018  divcn  25038  elcncf2  25060  mulc1cncf  25075  cncfmet  25079  evth2  25130  lmmbr2  25429  lmmbrf  25432  iscfil2  25436  cfil3i  25439  iscau2  25447  iscau4  25449  iscauf  25450  caucfil  25453  iscmet3lem3  25460  cfilres  25466  causs  25468  lmclim  25473  rrxmet  25578  evthicc2  25630  cniccbdd  25631  ovolfioo  25637  ovolficc  25638  ismbl2  25697  mbfsup  25834  mbfinf  25835  mbflimsup  25836  0plef  25842  mbfi1flim  25893  xrge0f  25901  itg2mulclem  25916  itgeqa  25984  ellimc2  26047  ellimc3  26049  limcflf  26051  cnlimc  26058  dvferm1  26155  dvferm2  26157  rolle  26160  dvivthlem1  26178  ftc1lem6  26211  itgsubst  26219  mdegle0  26245  deg1leb  26263  plydivex  26469  ulm2  26559  ulmcaulem  26568  ulmcau  26569  ulmdvlem3  26576  abelthlem9  26614  abelth  26615  rlimcnp  27141  ftalem3  27250  issqf  27311  sqf11  27314  mpodvdsmulf1o  27369  dvdsmulf1o  27371  dchrelbas4  27418  dchrinv  27436  2sqlem6  27598  chpo1ubb  27656  dchrmusumlema  27668  dchrisum0lema  27689  ostth3  27813  ltsrec  28005  lrrecfr  28147  addsuniflem  28205  addbday  28222  negsunif  28259  n0fincut  28559  bdayfinbndlem1  28671  elreno2  28699  tgcgr4  28811  eqeelen  29265  brbtwn2  29266  colinearalg  29271  axcgrid  29277  axsegconlem1  29278  ax5seglem4  29293  ax5seglem5  29294  axbtwnid  29300  axpasch  29302  axeuclidlem  29323  axcontlem2  29326  axcontlem4  29328  axcontlem7  29331  axcontlem12  29336  elntg2  29346  isuvtx  29756  uvtx2vtx1edg  29759  uvtx2vtx1edgb  29760  iscplgrnb  29777  iscplgredg  29778  vdiscusgrb  29891  uhgrvd00  29895  upgriswlk  30001  wwlksnext  30253  clwwlkinwwlk  30402  clwwlkel  30408  clwwlkf  30409  clwwlkwwlksb  30416  wwlksext2clwwlk  30419  wwlksubclwwlk  30420  clwwlknonex2lem2  30470  nmounbi  31139  blocnilem  31167  isph  31185  phoeqi  31220  h2hcau  31342  h2hlm  31343  hial2eq2  31470  hoeq1  32193  hoeq2  32194  adjsym  32196  cnvadj  32255  hhcno  32267  hhcnf  32268  adjvalval  32300  leop2  32487  leoptri  32499  mdbr2  32659  dmdbr2  32666  mddmd2  32672  cdj3lem3b  32803  infxrge0gelb  33122  prodindf  33193  toslublem  33301  tosglblem  33303  mgccnv  33328  cntrval2  33500  submarchi  33515  isarchi3  33516  lindfpropd  33704  opprlidlabs  33776  ply1moneq  33887  psrmonmul  33949  cmpcref  34249  lmdvg  34352  eulerpartlemd  34765  subfacp1lem3  35682  subfacp1lem5  35684  satfv1lem  35862  dfrdg2  36293  nadddilem2  36721  nadddilem4  36723  opnrebl  36859  poimirlem23  38322  broucube  38333  itg2gt0cn  38354  ftc1cnnc  38371  lmclim2  38437  caures  38439  sstotbnd2  38453  rrnmet  38508  rrncmslem  38511  isdrngo3  38638  isidlc  38694  cvrval2  40076  isat3  40109  iscvlat2N  40126  glbconN  40179  ltrneq  40951  cdlemefrs29clN  41201  cdlemefrs32fva  41202  cdleme32fva  41239  cdlemk33N  41711  cdlemk34  41712  cdlemkid3N  41735  cdlemkid4  41736  diaglbN  41857  dibglbN  41968  dihglbcpreN  42102  dihglblem6  42142  hdmap1eulem  42624  hdmap1eulemOLDN  42625  hdmapoc  42733  hlhilocv  42759  primrootsunit1  42892  sn-sup3d  43294  fimgmcyc  43330  wepwsolem  43797  fnwe2lem2  43806  islnm2  43833  onmaxnelsup  43978  onsupnmax  43983  onsupuni  43984  onsupmaxb  43994  onsupeqnmax  44002  iscard5  44290  alephiso2  44312  clsk3nimkb  44794  ntrclsneine0  44819  ntrneineine0  44841  ntrneineine1  44842  ntrneicls00  44843  ntrneicls11  44844  ntrneiiso  44845  ntrneik2  44846  ntrneix2  44847  ntrneikb  44848  ntrneixb  44849  ntrneik3  44850  ntrneix3  44851  ntrneik13  44852  ntrneix13  44853  ntrneik4w  44854  ntrneik4  44855  caofcan  45061  modelac8prim  45729  infxrbnd2  46112  supminfxr  46206  rexanuz2nf  46234  evthiccabs  46240  ellimcabssub0  46361  climf  46366  clim2f  46378  clim2cf  46392  clim0cf  46396  limsupmnflem  46462  limsupre2lem  46466  limsupreuzmpt  46481  supcnvlimsup  46482  limsupge  46503  liminfreuzlem  46544  liminfltlem  46546  liminflimsupclim  46549  liminfpnfuz  46558  xlimpnfxnegmnf2  46600  fourierdlem70  46918  fourierdlem71  46919  fourierdlem73  46921  fourierdlem80  46928  fourierdlem83  46931  fourierdlem87  46935  voliunsge0lem  47214  meaiuninclem  47222  meaiuninc3v  47226  hoidmv1lelem3  47335  hoidmvlelem4  47340  hoidmvlelem5  47341  issmflem  47469  chnerlem1  47626  cfsetsnfsetf  47823  cfsetsnfsetfo  47825  nprmmul1  48304  requad2  48416  isubgrgrim  48722  grlicref  48805  islinindfis  49257  elbigolo1  49365  line2x  49562  itscnhlinecirc02p  49593  iscnrm3lem1  49740  ipolublem  49792  ipoglblem  49795  oppcup  50013  uptrlem3  50018  initopropd  50049  termopropd  50050  isinito2lem  50304  termc2  50324  lanup  50447  ranup  50448  aacllem  50649