Theorem ralbidva 2433

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1480  ∀wral 2416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  raleqbidva  2640  poinxp  4608  funimass4  5472  funimass3  5536  funconstss  5538  cocan1  5688  cocan2  5689  isocnv2  5713  isores2  5714  isoini2  5720  ofrfval  5990  ofrfval2  5998  dfsmo2  6184  smores  6189  smores2  6191  ac6sfi  6792  supisolem  6895  ordiso2  6920  ismkvnex  7029  caucvgsrlemcau  7601  suplocsrlempr  7615  axsuploc  7837  suprleubex  8712  dfinfre  8714  zextlt  9143  prime  9150  fzshftral  9888  fimaxq  10573  clim  11050  clim2  11052  clim2c  11053  clim0c  11055  climabs0  11076  climrecvg1n  11117  mertenslem2  11305  mertensabs  11306  dfgcd2  11702  sqrt2irr  11840  tgss2  12248  neipsm  12323  ssidcn  12379  lmbrf  12384  cnnei  12401  cnrest2  12405  lmss  12415  lmres  12417  ismet2  12523  elmopn2  12618  metss  12663  metrest  12675  metcnp  12681  metcnp2  12682  metcn  12683  txmetcnp  12687  divcnap  12724  elcncf2  12730  mulc1cncf  12745  cncfmet  12748  cdivcncfap  12756  limcdifap  12800  limcmpted  12801  cnlimc  12810