Theorem ralbi 3061

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

Assertion

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

Proof of Theorem ralbi

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-12 2044

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-ral 2912

This theorem is referenced by:  uniiunlem  3669  iineq2  4504  reusv2lem5  4833  ralrnmpt  6324  f1mpt  6472  mpt22eqb  6722  ralrnmpt2  6728  rankonidlem  8635  acni2  8813  kmlem8  8923  kmlem13  8928  fimaxre3  10914  cau3lem  14028  rlim2  14161  rlim0  14173  rlim0lt  14174  catpropd  16290  funcres2b  16478  ulmss  24055  lgamgulmlem6  24660  colinearalg  25690  axpasch  25721  axcontlem2  25745  axcontlem4  25747  axcontlem7  25750  axcontlem8  25751  neibastop3  31996  ralbi12f  33598  iineq12f  33602  pmapglbx  34532  ordelordALTVD  38583