Theorem ralbi 3092

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

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

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

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

This theorem is referenced by:  rexbiOLD  3170  uniiunlem  4015  iineq2  4941  reusv2lem5  5320  ralrnmptw  6952  ralrnmpt  6954  f1mpt  7115  mpo2eqb  7384  ralrnmpo  7390  rankonidlem  9517  acni2  9733  kmlem8  9844  kmlem13  9849  fimaxre3  11851  cau3lem  14994  rlim2  15133  rlim0  15145  rlim0lt  15146  catpropd  17335  funcres2b  17528  ulmss  25461  lgamgulmlem6  26088  colinearalg  27181  axpasch  27212  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  axcontlem8  27242  naddcom  33762  naddid1  33763  neibastop3  34478  bj-0int  35199  ralbi12f  36245  iineq12f  36249  pmapglbx  37710  ordelordALTVD  42376