Theorem ralbidva 2471

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 1526	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	ralbida 2469	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

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

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458

This theorem is referenced by:  raleqbidva  2684  poinxp  4689  funimass4  5558  fnmptfvd  5612  funimass3  5624  funconstss  5626  cocan1  5778  cocan2  5779  isocnv2  5803  isores2  5804  isoini2  5810  ofrfval  6081  ofrfval2  6089  dfsmo2  6278  smores  6283  smores2  6285  ac6sfi  6888  supisolem  6997  ordiso2  7024  ismkvnex  7143  nninfwlporlemd  7160  caucvgsrlemcau  7767  suplocsrlempr  7781  axsuploc  8004  suprleubex  8884  dfinfre  8886  zextlt  9318  prime  9325  infregelbex  9571  fzshftral  10078  fimaxq  10775  clim  11257  clim2  11259  clim2c  11260  clim0c  11262  climabs0  11283  climrecvg1n  11324  mertenslem2  11512  mertensabs  11513  dfgcd2  11982  sqrt2irr  12129  pc11  12297  pcz  12298  1arith  12332  infpn2  12424  grpidpropdg  12668  mndpropd  12716  grppropd  12764  ringpropd  13022  oppr1g  13056  tgss2  13159  neipsm  13234  ssidcn  13290  lmbrf  13295  cnnei  13312  cnrest2  13316  lmss  13326  lmres  13328  ismet2  13434  elmopn2  13529  metss  13574  metrest  13586  metcnp  13592  metcnp2  13593  metcn  13594  txmetcnp  13598  divcnap  13635  elcncf2  13641  mulc1cncf  13656  cncfmet  13659  cdivcncfap  13667  limcdifap  13711  limcmpted  13712  cnlimc  13721  2sqlem6  14036  iswomni0  14369