Theorem ralbidva 2546

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  raleqbidva  2767  poinxp  4844  funimass4  5753  fnmptfvd  5813  funimass3  5825  funconstss  5827  cocan1  5993  cocan2  5994  isocnv2  6018  isores2  6019  isoini2  6025  ofrfval  6311  ofrfval2  6319  dfsmo2  6558  smores  6563  smores2  6565  ac6sfi  7202  supisolem  7349  ordiso2  7376  ismkvnex  7496  nninfwlporlemd  7513  caucvgsrlemcau  8161  suplocsrlempr  8175  axsuploc  8399  suprleubex  9287  dfinfre  9289  zextlt  9743  prime  9750  infregelbex  10008  fzshftral  10526  nninfinf  10895  fimaxq  11286  swrdspsleq  11455  pfxeq  11484  clim  12066  clim2  12068  clim2c  12069  clim0c  12071  climabs0  12092  climrecvg1n  12133  mertenslem2  12322  mertensabs  12323  dfgcd2  12810  sqrt2irr  12960  pc11  13133  pcz  13134  1arith  13169  ballotfilemodife  13292  infpn2  13399  grpidpropdg  13747  sgrppropd  13781  mndpropd  13806  grppropd  13875  issubg4m  14049  rngpropd  14338  ringpropd  14427  oppr1g  14472  opprdrng  14704  lsspropdg  14852  isridlrng  14903  isridl  14925  expghmap  15026  assapropd  15098  psrbagconf1o  15149  tgss2  15271  neipsm  15346  ssidcn  15402  lmbrf  15407  cnnei  15424  cnrest2  15428  lmss  15438  lmres  15440  ismet2  15546  elmopn2  15641  metss  15686  metrest  15698  metcnp  15704  metcnp2  15705  metcn  15706  txmetcnp  15710  divcnap  15757  elcncf2  15766  mulc1cncf  15781  cncfmet  15784  cdivcncfap  15796  limcdifap  15854  limcmpted  15855  cnlimc  15864  mpodvdsmulf1o  16245  2sqlem6  16405  upgriswlkdc  16767  clwwlknonex2lem2  16845  iswomni0  17268  cndcap  17276