Theorem ralbi 3104

Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1821. (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 214	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
2	1	ral2imi 3086	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
3		biimpr 219	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
4	3	ral2imi 3086	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑))
5	2, 4	impbid 211	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  rexbiOLD  3106  uniiunlem  4085  iineq2  5018  reusv2lem5  5401  ralrnmptw  7096  ralrnmpt  7098  f1mpt  7260  mpo2eqb  7541  ralrnmpo  7547  naddcom  8681  naddrid  8682  naddass  8695  rankonidlem  9823  acni2  10041  kmlem8  10152  kmlem13  10157  fimaxre3  12160  cau3lem  15301  rlim2  15440  rlim0  15452  rlim0lt  15453  catpropd  17653  funcres2b  17847  ulmss  25909  lgamgulmlem6  26538  colinearalg  28168  axpasch  28199  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  axcontlem8  28229  neibastop3  35247  bj-0int  35982  ralbi12f  37028  iineq12f  37032  pmapglbx  38640  ordelordALTVD  43628