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  4744  funimass4  5629  fnmptfvd  5684  funimass3  5696  funconstss  5698  cocan1  5856  cocan2  5857  isocnv2  5881  isores2  5882  isoini2  5888  ofrfval  6167  ofrfval2  6175  dfsmo2  6373  smores  6378  smores2  6380  ac6sfi  6995  supisolem  7110  ordiso2  7137  ismkvnex  7257  nninfwlporlemd  7274  caucvgsrlemcau  7906  suplocsrlempr  7920  axsuploc  8145  suprleubex  9027  dfinfre  9029  zextlt  9465  prime  9472  infregelbex  9719  fzshftral  10230  nninfinf  10588  fimaxq  10972  swrdspsleq  11120  clim  11592  clim2  11594  clim2c  11595  clim0c  11597  climabs0  11618  climrecvg1n  11659  mertenslem2  11847  mertensabs  11848  dfgcd2  12335  sqrt2irr  12484  pc11  12654  pcz  12655  1arith  12690  infpn2  12827  grpidpropdg  13206  sgrppropd  13245  mndpropd  13272  grppropd  13349  issubg4m  13529  rngpropd  13717  ringpropd  13800  oppr1g  13844  lsspropdg  14193  isridlrng  14244  isridl  14266  expghmap  14369  tgss2  14551  neipsm  14626  ssidcn  14682  lmbrf  14687  cnnei  14704  cnrest2  14708  lmss  14718  lmres  14720  ismet2  14826  elmopn2  14921  metss  14966  metrest  14978  metcnp  14984  metcnp2  14985  metcn  14986  txmetcnp  14990  divcnap  15037  elcncf2  15046  mulc1cncf  15061  cncfmet  15064  cdivcncfap  15076  limcdifap  15134  limcmpted  15135  cnlimc  15144  mpodvdsmulf1o  15462  2sqlem6  15597  iswomni0  15990  cndcap  15998