Theorem ralbi 3170

Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1859. (Contributed by NM, 6-Oct-2003.)

Assertion

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

Proof of Theorem ralbi

Step	Hyp	Ref	Expression
1		nfra1 3043	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)
2		rspa 3032	. 2 ⊢ ((∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓))
3	1, 2	ralbida 3084	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 196  ∀wral 3014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-10 2132  ax-12 2160

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1818  df-nf 1823  df-ral 3019

This theorem is referenced by:  uniiunlem  3798  iineq2  4646  reusv2lem5  4978  ralrnmpt  6483  f1mpt  6633  mpt22eqb  6886  ralrnmpt2  6892  rankonidlem  8804  acni2  8982  kmlem8  9092  kmlem13  9097  fimaxre3  11083  cau3lem  14214  rlim2  14347  rlim0  14359  rlim0lt  14360  catpropd  16491  funcres2b  16679  ulmss  24271  lgamgulmlem6  24880  colinearalg  25910  axpasch  25941  axcontlem2  25965  axcontlem4  25967  axcontlem7  25970  axcontlem8  25971  neibastop3  32584  bj-0int  33282  ralbi12f  34201  iineq12f  34205  pmapglbx  35475  ordelordALTVD  39519