Theorem ralbi 3134

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wral 3105

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

This theorem depends on definitions:  df-bi 208  df-ral 3110

This theorem is referenced by:  uniiunlem  3982  iineq2  4844  reusv2lem5  5194  ralrnmpt  6725  f1mpt  6884  mpo2eqb  7139  ralrnmpo  7145  rankonidlem  9103  acni2  9318  kmlem8  9429  kmlem13  9434  fimaxre3  11435  cau3lem  14548  rlim2  14687  rlim0  14699  rlim0lt  14700  catpropd  16808  funcres2b  16996  ulmss  24668  lgamgulmlem6  25293  colinearalg  26379  axpasch  26410  axcontlem2  26434  axcontlem4  26436  axcontlem7  26439  axcontlem8  26440  neibastop3  33320  bj-0int  34011  ralbi12f  34989  iineq12f  34993  pmapglbx  36455  ordelordALTVD  40759