Theorem ralbidva 2528

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ralbidva	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidva

Step	Hyp	Ref	Expression
1		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	ralbida 2526	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2202  ∀wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  raleqbidva  2748  poinxp  4795  funimass4  5696  fnmptfvd  5751  funimass3  5763  funconstss  5765  cocan1  5928  cocan2  5929  isocnv2  5953  isores2  5954  isoini2  5960  ofrfval  6244  ofrfval2  6252  dfsmo2  6453  smores  6458  smores2  6460  ac6sfi  7087  supisolem  7207  ordiso2  7234  ismkvnex  7354  nninfwlporlemd  7371  caucvgsrlemcau  8013  suplocsrlempr  8027  axsuploc  8252  suprleubex  9134  dfinfre  9136  zextlt  9572  prime  9579  infregelbex  9832  fzshftral  10343  nninfinf  10706  fimaxq  11092  swrdspsleq  11252  pfxeq  11281  clim  11859  clim2  11861  clim2c  11862  clim0c  11864  climabs0  11885  climrecvg1n  11926  mertenslem2  12115  mertensabs  12116  dfgcd2  12603  sqrt2irr  12752  pc11  12922  pcz  12923  1arith  12958  infpn2  13095  grpidpropdg  13475  sgrppropd  13514  mndpropd  13541  grppropd  13618  issubg4m  13798  rngpropd  13987  ringpropd  14070  oppr1g  14114  lsspropdg  14464  isridlrng  14515  isridl  14537  expghmap  14640  tgss2  14822  neipsm  14897  ssidcn  14953  lmbrf  14958  cnnei  14975  cnrest2  14979  lmss  14989  lmres  14991  ismet2  15097  elmopn2  15192  metss  15237  metrest  15249  metcnp  15255  metcnp2  15256  metcn  15257  txmetcnp  15261  divcnap  15308  elcncf2  15317  mulc1cncf  15332  cncfmet  15335  cdivcncfap  15347  limcdifap  15405  limcmpted  15406  cnlimc  15415  mpodvdsmulf1o  15733  2sqlem6  15868  upgriswlkdc  16230  clwwlknonex2lem2  16308  iswomni0  16707  cndcap  16715