Theorem ralbidva 2473

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  raleqbidva  2687  poinxp  4697  funimass4  5568  fnmptfvd  5622  funimass3  5634  funconstss  5636  cocan1  5790  cocan2  5791  isocnv2  5815  isores2  5816  isoini2  5822  ofrfval  6093  ofrfval2  6101  dfsmo2  6290  smores  6295  smores2  6297  ac6sfi  6900  supisolem  7009  ordiso2  7036  ismkvnex  7155  nninfwlporlemd  7172  caucvgsrlemcau  7794  suplocsrlempr  7808  axsuploc  8032  suprleubex  8913  dfinfre  8915  zextlt  9347  prime  9354  infregelbex  9600  fzshftral  10110  fimaxq  10809  clim  11291  clim2  11293  clim2c  11294  clim0c  11296  climabs0  11317  climrecvg1n  11358  mertenslem2  11546  mertensabs  11547  dfgcd2  12017  sqrt2irr  12164  pc11  12332  pcz  12333  1arith  12367  infpn2  12459  grpidpropdg  12798  mndpropd  12846  grppropd  12898  issubg4m  13058  ringpropd  13222  oppr1g  13257  lsspropdg  13522  tgss2  13664  neipsm  13739  ssidcn  13795  lmbrf  13800  cnnei  13817  cnrest2  13821  lmss  13831  lmres  13833  ismet2  13939  elmopn2  14034  metss  14079  metrest  14091  metcnp  14097  metcnp2  14098  metcn  14099  txmetcnp  14103  divcnap  14140  elcncf2  14146  mulc1cncf  14161  cncfmet  14164  cdivcncfap  14172  limcdifap  14216  limcmpted  14217  cnlimc  14226  2sqlem6  14552  iswomni0  14884  cndcap  14892