Theorem ralbi 3100

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

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

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

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

This theorem is referenced by:  rexbiOLD  3102  uniiunlem  4022  iineq2  4947  reusv2lem5  5328  ralrnmptw  6990  ralrnmpt  6992  f1mpt  7154  mpo2eqb  7426  ralrnmpo  7432  rankonidlem  9614  acni2  9830  kmlem8  9941  kmlem13  9946  fimaxre3  11949  cau3lem  15094  rlim2  15233  rlim0  15245  rlim0lt  15246  catpropd  17446  funcres2b  17640  ulmss  25584  lgamgulmlem6  26211  colinearalg  27306  axpasch  27337  axcontlem2  27361  axcontlem4  27363  axcontlem7  27366  axcontlem8  27367  naddcom  33863  naddid1  33864  neibastop3  34579  bj-0int  35300  ralbi12f  36346  iineq12f  36350  pmapglbx  37809  ordelordALTVD  42511