Theorem ralbidva 2502

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  raleqbidva  2720  poinxp  4745  funimass4  5631  fnmptfvd  5686  funimass3  5698  funconstss  5700  cocan1  5858  cocan2  5859  isocnv2  5883  isores2  5884  isoini2  5890  ofrfval  6169  ofrfval2  6177  dfsmo2  6375  smores  6380  smores2  6382  ac6sfi  6997  supisolem  7112  ordiso2  7139  ismkvnex  7259  nninfwlporlemd  7276  caucvgsrlemcau  7908  suplocsrlempr  7922  axsuploc  8147  suprleubex  9029  dfinfre  9031  zextlt  9467  prime  9474  infregelbex  9721  fzshftral  10232  nninfinf  10590  fimaxq  10974  swrdspsleq  11123  pfxeq  11150  clim  11625  clim2  11627  clim2c  11628  clim0c  11630  climabs0  11651  climrecvg1n  11692  mertenslem2  11880  mertensabs  11881  dfgcd2  12368  sqrt2irr  12517  pc11  12687  pcz  12688  1arith  12723  infpn2  12860  grpidpropdg  13239  sgrppropd  13278  mndpropd  13305  grppropd  13382  issubg4m  13562  rngpropd  13750  ringpropd  13833  oppr1g  13877  lsspropdg  14226  isridlrng  14277  isridl  14299  expghmap  14402  tgss2  14584  neipsm  14659  ssidcn  14715  lmbrf  14720  cnnei  14737  cnrest2  14741  lmss  14751  lmres  14753  ismet2  14859  elmopn2  14954  metss  14999  metrest  15011  metcnp  15017  metcnp2  15018  metcn  15019  txmetcnp  15023  divcnap  15070  elcncf2  15079  mulc1cncf  15094  cncfmet  15097  cdivcncfap  15109  limcdifap  15167  limcmpted  15168  cnlimc  15177  mpodvdsmulf1o  15495  2sqlem6  15630  iswomni0  16027  cndcap  16035