Theorem ralbi 3170

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wral 3141

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 209  df-ral 3146

This theorem is referenced by:  uniiunlem  4064  iineq2  4942  reusv2lem5  5306  ralrnmptw  6863  ralrnmpt  6865  f1mpt  7022  mpo2eqb  7286  ralrnmpo  7292  rankonidlem  9260  acni2  9475  kmlem8  9586  kmlem13  9591  fimaxre3  11590  cau3lem  14717  rlim2  14856  rlim0  14868  rlim0lt  14869  catpropd  16982  funcres2b  17170  ulmss  24988  lgamgulmlem6  25614  colinearalg  26699  axpasch  26730  axcontlem2  26754  axcontlem4  26756  axcontlem7  26759  axcontlem8  26760  neibastop3  33714  bj-0int  34397  ralbi12f  35442  iineq12f  35446  pmapglbx  36909  ordelordALTVD  41207