Theorem ralbi 3085

Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1818. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)

Assertion

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

Proof of Theorem ralbi

Step	Hyp	Ref	Expression
1		biimp 215	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
2	1	ral2imi 3068	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
3		biimpr 220	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
4	3	ral2imi 3068	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑))
5	2, 4	impbid 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  uniiunlem  4046  iineq2  4972  reusv2lem5  5352  ralrnmptw  7048  ralrnmpt  7050  f1mpt  7218  mpo2eqb  7501  ralrnmpo  7508  naddcom  8623  naddrid  8624  naddass  8637  rankonidlem  9757  acni2  9975  kmlem8  10087  kmlem13  10092  fimaxre3  12105  cau3lem  15297  rlim2  15438  rlim0  15450  rlim0lt  15451  catpropd  17650  funcres2b  17839  ulmss  26339  lgamgulmlem6  26977  colinearalg  28890  axpasch  28921  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  axcontlem8  28951  neibastop3  36343  bj-0int  37082  ralbi12f  38147  iineq12f  38151  pmapglbx  39756  ordelordALTVD  44849