Theorem ralbi 3117

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

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

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

This theorem depends on definitions:  df-bi 209  df-ral 3077

This theorem is referenced by:  uniiunlem  4040  iineq2  4970  reusv2lem5  5359  ralrnmptw  7075  ralrnmpt  7077  f1mpt  7245  mpo2eqb  7528  ralrnmpo  7535  naddcom  8653  naddrid  8654  naddass  8667  rankonidlem  9786  acni2  10002  kmlem8  10114  kmlem13  10119  fimaxre3  12138  cau3lem  15382  rlim2  15523  rlim0  15535  rlim0lt  15536  catpropd  17741  funcres2b  17930  ulmss  26460  lgamgulmlem6  27098  colinearalg  29111  axpasch  29142  axcontlem2  29166  axcontlem4  29168  axcontlem7  29171  axcontlem8  29172  neibastop3  36722  bj-0int  37591  ralbi12f  38659  iineq12f  38663  pmapglbx  40393  ordelordALTVD  45442