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  17646  funcres2b  17835  ulmss  26282  lgamgulmlem6  26920  colinearalg  28813  axpasch  28844  axcontlem2  28868  axcontlem4  28870  axcontlem7  28873  axcontlem8  28874  neibastop3  36323  bj-0int  37062  ralbi12f  38127  iineq12f  38131  pmapglbx  39736  ordelordALTVD  44829