Theorem ralbi 3092

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3051

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

This theorem depends on definitions:  df-bi 207  df-ral 3052

This theorem is referenced by:  uniiunlem  4027  iineq2  4954  reusv2lem5  5344  ralrnmptw  7046  ralrnmpt  7048  f1mpt  7216  mpo2eqb  7499  ralrnmpo  7506  naddcom  8618  naddrid  8619  naddass  8632  rankonidlem  9752  acni2  9968  kmlem8  10080  kmlem13  10085  fimaxre3  12102  cau3lem  15317  rlim2  15458  rlim0  15470  rlim0lt  15471  catpropd  17675  funcres2b  17864  ulmss  26362  lgamgulmlem6  26997  colinearalg  28979  axpasch  29010  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  neibastop3  36544  bj-0int  37413  ralbi12f  38481  iineq12f  38485  pmapglbx  40215  ordelordALTVD  45293