Theorem ralbidva 2486

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473

This theorem is referenced by:  raleqbidva  2700  poinxp  4713  funimass4  5587  fnmptfvd  5641  funimass3  5653  funconstss  5655  cocan1  5809  cocan2  5810  isocnv2  5834  isores2  5835  isoini2  5841  ofrfval  6116  ofrfval2  6124  dfsmo2  6313  smores  6318  smores2  6320  ac6sfi  6927  supisolem  7038  ordiso2  7065  ismkvnex  7184  nninfwlporlemd  7201  caucvgsrlemcau  7823  suplocsrlempr  7837  axsuploc  8061  suprleubex  8942  dfinfre  8944  zextlt  9376  prime  9383  infregelbex  9630  fzshftral  10140  fimaxq  10842  clim  11324  clim2  11326  clim2c  11327  clim0c  11329  climabs0  11350  climrecvg1n  11391  mertenslem2  11579  mertensabs  11580  dfgcd2  12050  sqrt2irr  12197  pc11  12366  pcz  12367  1arith  12402  infpn2  12510  grpidpropdg  12853  sgrppropd  12891  mndpropd  12916  grppropd  12977  issubg4m  13149  rngpropd  13326  ringpropd  13409  oppr1g  13449  lsspropdg  13764  isridlrng  13815  isridl  13836  tgss2  14056  neipsm  14131  ssidcn  14187  lmbrf  14192  cnnei  14209  cnrest2  14213  lmss  14223  lmres  14225  ismet2  14331  elmopn2  14426  metss  14471  metrest  14483  metcnp  14489  metcnp2  14490  metcn  14491  txmetcnp  14495  divcnap  14532  elcncf2  14538  mulc1cncf  14553  cncfmet  14556  cdivcncfap  14564  limcdifap  14608  limcmpted  14609  cnlimc  14618  2sqlem6  14945  iswomni0  15278  cndcap  15286