Theorem ralbi 3093

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

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

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

This theorem depends on definitions:  df-bi 207  df-ral 3053

This theorem is referenced by:  uniiunlem  4028  iineq2  4955  reusv2lem5  5340  ralrnmptw  7041  ralrnmpt  7043  f1mpt  7210  mpo2eqb  7493  ralrnmpo  7500  naddcom  8612  naddrid  8613  naddass  8626  rankonidlem  9746  acni2  9962  kmlem8  10074  kmlem13  10079  fimaxre3  12096  cau3lem  15311  rlim2  15452  rlim0  15464  rlim0lt  15465  catpropd  17669  funcres2b  17858  ulmss  26378  lgamgulmlem6  27014  colinearalg  28996  axpasch  29027  axcontlem2  29051  axcontlem4  29053  axcontlem7  29056  axcontlem8  29057  neibastop3  36563  bj-0int  37432  ralbi12f  38498  iineq12f  38502  pmapglbx  40232  ordelordALTVD  45314