Theorem ralbidva 2434

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

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

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  raleqbidva  2643  poinxp  4616  funimass4  5480  funimass3  5544  funconstss  5546  cocan1  5696  cocan2  5697  isocnv2  5721  isores2  5722  isoini2  5728  ofrfval  5998  ofrfval2  6006  dfsmo2  6192  smores  6197  smores2  6199  ac6sfi  6800  supisolem  6903  ordiso2  6928  ismkvnex  7037  caucvgsrlemcau  7625  suplocsrlempr  7639  axsuploc  7861  suprleubex  8736  dfinfre  8738  zextlt  9167  prime  9174  fzshftral  9919  fimaxq  10605  clim  11082  clim2  11084  clim2c  11085  clim0c  11087  climabs0  11108  climrecvg1n  11149  mertenslem2  11337  mertensabs  11338  dfgcd2  11738  sqrt2irr  11876  tgss2  12287  neipsm  12362  ssidcn  12418  lmbrf  12423  cnnei  12440  cnrest2  12444  lmss  12454  lmres  12456  ismet2  12562  elmopn2  12657  metss  12702  metrest  12714  metcnp  12720  metcnp2  12721  metcn  12722  txmetcnp  12726  divcnap  12763  elcncf2  12769  mulc1cncf  12784  cncfmet  12787  cdivcncfap  12795  limcdifap  12839  limcmpted  12840  cnlimc  12849