Theorem ralbidva 2376

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

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∈ wcel 1438  ∀wral 2359

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364

This theorem is referenced by:  raleqbidva  2576  poinxp  4495  funimass4  5339  funimass3  5399  funconstss  5401  cocan1  5548  cocan2  5549  isocnv2  5573  isores2  5574  isoini2  5580  ofrfval  5846  ofrfval2  5853  dfsmo2  6034  smores  6039  smores2  6041  ac6sfi  6594  supisolem  6682  ordiso2  6707  caucvgsrlemcau  7317  suprleubex  8387  dfinfre  8389  zextlt  8808  prime  8815  fzshftral  9489  fimaxq  10200  clim  10633  clim2  10635  clim2c  10636  clim0c  10638  climabs0  10660  climrecvg1n  10701  dfgcd2  11085  sqrt2irr  11223