Theorem ralbi 3119

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  uniiunlem  4038  iineq2  4975  reusv2lem5  5371  ralrnmptw  7090  ralrnmpt  7092  f1mpt  7261  mpo2eqb  7548  ralrnmpo  7555  naddcom  8674  naddrid  8675  naddass  8688  rankonidlem  9813  acni2  10052  kmlem8  10163  kmlem13  10168  fimaxre3  12186  cau3lem  15442  rlim2  15583  rlim0  15595  rlim0lt  15596  catpropd  17799  funcres2b  17988  ulmss  26628  lgamgulmlem6  27266  colinearalg  29351  axpasch  29382  axcontlem2  29406  axcontlem4  29408  axcontlem7  29411  axcontlem8  29412  nmulrid  36762  neibastop3  36966  bj-0int  37836  ralbi12f  38893  iineq12f  38897  pmapglbx  40627  ordelordALTVD  45674