Theorem ralbidva 2526

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  raleqbidva  2746  poinxp  4788  funimass4  5684  fnmptfvd  5739  funimass3  5751  funconstss  5753  cocan1  5911  cocan2  5912  isocnv2  5936  isores2  5937  isoini2  5943  ofrfval  6227  ofrfval2  6235  dfsmo2  6433  smores  6438  smores2  6440  ac6sfi  7060  supisolem  7175  ordiso2  7202  ismkvnex  7322  nninfwlporlemd  7339  caucvgsrlemcau  7980  suplocsrlempr  7994  axsuploc  8219  suprleubex  9101  dfinfre  9103  zextlt  9539  prime  9546  infregelbex  9793  fzshftral  10304  nninfinf  10665  fimaxq  11049  swrdspsleq  11199  pfxeq  11228  clim  11792  clim2  11794  clim2c  11795  clim0c  11797  climabs0  11818  climrecvg1n  11859  mertenslem2  12047  mertensabs  12048  dfgcd2  12535  sqrt2irr  12684  pc11  12854  pcz  12855  1arith  12890  infpn2  13027  grpidpropdg  13407  sgrppropd  13446  mndpropd  13473  grppropd  13550  issubg4m  13730  rngpropd  13918  ringpropd  14001  oppr1g  14045  lsspropdg  14395  isridlrng  14446  isridl  14468  expghmap  14571  tgss2  14753  neipsm  14828  ssidcn  14884  lmbrf  14889  cnnei  14906  cnrest2  14910  lmss  14920  lmres  14922  ismet2  15028  elmopn2  15123  metss  15168  metrest  15180  metcnp  15186  metcnp2  15187  metcn  15188  txmetcnp  15192  divcnap  15239  elcncf2  15248  mulc1cncf  15263  cncfmet  15266  cdivcncfap  15278  limcdifap  15336  limcmpted  15337  cnlimc  15346  mpodvdsmulf1o  15664  2sqlem6  15799  upgriswlkdc  16071  iswomni0  16419  cndcap  16427