Theorem ralbi 3086

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 3069	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
3		biimpr 220	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
4	3	ral2imi 3069	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑))
5	2, 4	impbid 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))

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

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 3046

This theorem is referenced by:  uniiunlem  4053  iineq2  4979  reusv2lem5  5360  ralrnmptw  7069  ralrnmpt  7071  f1mpt  7239  mpo2eqb  7524  ralrnmpo  7531  naddcom  8649  naddrid  8650  naddass  8663  rankonidlem  9788  acni2  10006  kmlem8  10118  kmlem13  10123  fimaxre3  12136  cau3lem  15328  rlim2  15469  rlim0  15481  rlim0lt  15482  catpropd  17677  funcres2b  17866  ulmss  26313  lgamgulmlem6  26951  colinearalg  28844  axpasch  28875  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  neibastop3  36357  bj-0int  37096  ralbi12f  38161  iineq12f  38165  pmapglbx  39770  ordelordALTVD  44863