Theorem ralbid 3279

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3189. (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 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	ralbida 3277	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3081

This theorem is used by:  raleqbid  3347  sbcralt  3823  sbcrext  3824  riota5f  7428  zfrep6OLD  7991  cnfcom3clem  9733  cplem2  9979  cplem2OLD  9980  infxpenc2lem2  10126  acnlem  10154  lble  12296  fsuppmapnn0fiubex  14162  nosupbnd1  28101  noinfbnd1  28116  chirred  33027  rspc2daf  33135  aciunf1lem  33328  srepdflem2  36086  indexa  38859  riotasvd  40205  cdlemk36  42162  modelaxreplem3  46165  choicefi  46419  axccdom  46440  rexabsle  46634  infxrunb3rnmpt  46643  uzublem  46645  climf  46839  climf2  46881  limsupubuzlem  46927  cncficcgt0  47103  stoweidlem16  47231  stoweidlem18  47233  stoweidlem21  47236  stoweidlem29  47244  stoweidlem31  47246  stoweidlem36  47251  stoweidlem41  47256  stoweidlem44  47259  stoweidlem45  47260  stoweidlem51  47266  stoweidlem55  47270  stoweidlem59  47274  stoweidlem60  47275  issmfgelem  47984  smfpimcclem  48022  sprsymrelf  48782