Theorem ralbi 3084

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

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

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 3045

This theorem is referenced by:  uniiunlem  4038  iineq2  4962  reusv2lem5  5341  ralrnmptw  7028  ralrnmpt  7030  f1mpt  7198  mpo2eqb  7481  ralrnmpo  7488  naddcom  8600  naddrid  8601  naddass  8614  rankonidlem  9724  acni2  9940  kmlem8  10052  kmlem13  10057  fimaxre3  12071  cau3lem  15262  rlim2  15403  rlim0  15415  rlim0lt  15416  catpropd  17615  funcres2b  17804  ulmss  26304  lgamgulmlem6  26942  colinearalg  28855  axpasch  28886  axcontlem2  28910  axcontlem4  28912  axcontlem7  28915  axcontlem8  28916  neibastop3  36346  bj-0int  37085  ralbi12f  38150  iineq12f  38154  pmapglbx  39758  ordelordALTVD  44850