Theorem ralbidva 2538

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525

This theorem is referenced by:  raleqbidva  2759  poinxp  4819  funimass4  5727  fnmptfvd  5782  funimass3  5794  funconstss  5796  cocan1  5960  cocan2  5961  isocnv2  5985  isores2  5986  isoini2  5992  ofrfval  6275  ofrfval2  6283  dfsmo2  6518  smores  6523  smores2  6525  ac6sfi  7155  supisolem  7299  ordiso2  7326  ismkvnex  7446  nninfwlporlemd  7463  caucvgsrlemcau  8108  suplocsrlempr  8122  axsuploc  8346  suprleubex  9228  dfinfre  9230  zextlt  9670  prime  9677  infregelbex  9930  fzshftral  10442  nninfinf  10805  fimaxq  11194  swrdspsleq  11359  pfxeq  11388  clim  11966  clim2  11968  clim2c  11969  clim0c  11971  climabs0  11992  climrecvg1n  12033  mertenslem2  12222  mertensabs  12223  dfgcd2  12710  sqrt2irr  12859  pc11  13029  pcz  13030  1arith  13065  infpn2  13207  grpidpropdg  13587  sgrppropd  13626  mndpropd  13653  grppropd  13730  issubg4m  13910  rngpropd  14099  ringpropd  14182  oppr1g  14226  lsspropdg  14579  isridlrng  14630  isridl  14652  expghmap  14755  psrbagconf1o  14828  tgss2  14944  neipsm  15019  ssidcn  15075  lmbrf  15080  cnnei  15097  cnrest2  15101  lmss  15111  lmres  15113  ismet2  15219  elmopn2  15314  metss  15359  metrest  15371  metcnp  15377  metcnp2  15378  metcn  15379  txmetcnp  15383  divcnap  15430  elcncf2  15439  mulc1cncf  15454  cncfmet  15457  cdivcncfap  15469  limcdifap  15527  limcmpted  15528  cnlimc  15537  mpodvdsmulf1o  15858  2sqlem6  15993  upgriswlkdc  16355  clwwlknonex2lem2  16433  iswomni0  16836  cndcap  16844