Theorem ralbi 3097

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

Assertion

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

Proof of Theorem ralbi

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-ral 2946

This theorem is referenced by:  uniiunlem  3724  iineq2  4570  reusv2lem5  4903  ralrnmpt  6408  f1mpt  6558  mpt22eqb  6811  ralrnmpt2  6817  rankonidlem  8729  acni2  8907  kmlem8  9017  kmlem13  9022  fimaxre3  11008  cau3lem  14138  rlim2  14271  rlim0  14283  rlim0lt  14284  catpropd  16416  funcres2b  16604  ulmss  24196  lgamgulmlem6  24805  colinearalg  25835  axpasch  25866  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  neibastop3  32482  bj-0int  33180  ralbi12f  34099  iineq12f  34103  pmapglbx  35373  ordelordALTVD  39417