Theorem ralbid 3233

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)

Hypotheses

Ref	Expression
ralbid.1	⊢ Ⅎ𝑥𝜑
ralbid.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ralbid	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Proof of Theorem ralbid

Step	Hyp	Ref	Expression
1		ralbid.1	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbid.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	adantr 483	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	ralbida 3232	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1784   ∈ wcel 2114  ∀wral 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-ral 3145

This theorem is referenced by:  raleqbid  3423  sbcralt  3857  sbcrext  3858  riota5f  7144  zfrep6  7658  cnfcom3clem  9170  cplem2  9321  infxpenc2lem2  9448  acnlem  9476  lble  11595  fsuppmapnn0fiubex  13363  chirred  30174  rspc2daf  30233  aciunf1lem  30409  nosupbnd1  33216  indexa  35010  riotasvd  36094  cdlemk36  38051  choicefi  41470  axccdom  41494  rexabsle  41700  infxrunb3rnmpt  41709  uzublem  41711  climf  41910  climf2  41954  limsupubuzlem  42000  cncficcgt0  42178  stoweidlem16  42308  stoweidlem18  42310  stoweidlem21  42313  stoweidlem29  42321  stoweidlem31  42323  stoweidlem36  42328  stoweidlem41  42333  stoweidlem44  42336  stoweidlem45  42337  stoweidlem51  42343  stoweidlem55  42347  stoweidlem59  42351  stoweidlem60  42352  issmfgelem  43052  smfpimcclem  43088  sprsymrelf  43664