Theorem ralbidva 2540

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  raleqbidva  2761  poinxp  4826  funimass4  5734  fnmptfvd  5789  funimass3  5801  funconstss  5803  cocan1  5968  cocan2  5969  isocnv2  5993  isores2  5994  isoini2  6000  ofrfval  6286  ofrfval2  6294  dfsmo2  6533  smores  6538  smores2  6540  ac6sfi  7170  supisolem  7314  ordiso2  7341  ismkvnex  7461  nninfwlporlemd  7478  caucvgsrlemcau  8126  suplocsrlempr  8140  axsuploc  8364  suprleubex  9250  dfinfre  9252  zextlt  9693  prime  9700  infregelbex  9953  fzshftral  10469  nninfinf  10834  fimaxq  11224  swrdspsleq  11389  pfxeq  11418  clim  11997  clim2  11999  clim2c  12000  clim0c  12002  climabs0  12023  climrecvg1n  12064  mertenslem2  12253  mertensabs  12254  dfgcd2  12741  sqrt2irr  12890  pc11  13060  pcz  13061  1arith  13096  ballotfilemodife  13190  infpn2  13297  grpidpropdg  13643  sgrppropd  13682  mndpropd  13707  grppropd  13778  issubg4m  13952  rngpropd  14200  ringpropd  14287  oppr1g  14332  opprdrng  14564  lsspropdg  14711  isridlrng  14762  isridl  14784  expghmap  14887  psrbagconf1o  14960  tgss2  15076  neipsm  15151  ssidcn  15207  lmbrf  15212  cnnei  15229  cnrest2  15233  lmss  15243  lmres  15245  ismet2  15351  elmopn2  15446  metss  15491  metrest  15503  metcnp  15509  metcnp2  15510  metcn  15511  txmetcnp  15515  divcnap  15562  elcncf2  15571  mulc1cncf  15586  cncfmet  15589  cdivcncfap  15601  limcdifap  15659  limcmpted  15660  cnlimc  15669  mpodvdsmulf1o  15990  2sqlem6  16125  upgriswlkdc  16487  clwwlknonex2lem2  16565  iswomni0  16978  cndcap  16986