Theorem ralbi 3117

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

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

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 3077

This theorem is used by:  uniiunlem  4035  iineq2  4972  reusv2lem5  5367  ralrnmptw  7090  ralrnmpt  7092  f1mpt  7261  mpo2eqb  7548  ralrnmpo  7555  naddcom  8678  naddrid  8679  naddass  8692  rankonidlem  9817  acni2  10074  kmlem8  10185  kmlem13  10190  fimaxre3  12210  cau3lem  15467  rlim2  15608  rlim0  15620  rlim0lt  15621  catpropd  17822  funcres2b  18011  ulmss  26665  lgamgulmlem6  27302  colinearalg  29399  axpasch  29430  axcontlem2  29454  axcontlem4  29456  axcontlem7  29459  axcontlem8  29460  nmulrid  36844  neibastop3  37048  bj-0int  37918  ralbi12f  38973  iineq12f  38977  pmapglbx  40707  ordelordALTVD  45754