Theorem ralbi 3103

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

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

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 3062

This theorem is referenced by:  rexbiOLD  3105  uniiunlem  4087  iineq2  5012  reusv2lem5  5402  ralrnmptw  7114  ralrnmpt  7116  f1mpt  7281  mpo2eqb  7565  ralrnmpo  7572  naddcom  8720  naddrid  8721  naddass  8734  rankonidlem  9868  acni2  10086  kmlem8  10198  kmlem13  10203  fimaxre3  12214  cau3lem  15393  rlim2  15532  rlim0  15544  rlim0lt  15545  catpropd  17752  funcres2b  17942  ulmss  26440  lgamgulmlem6  27077  colinearalg  28925  axpasch  28956  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  axcontlem8  28986  neibastop3  36363  bj-0int  37102  ralbi12f  38167  iineq12f  38171  pmapglbx  39771  ordelordALTVD  44887