Theorem ralbi 3087

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

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

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

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

This theorem is referenced by:  uniiunlem  4034  iineq2  4960  reusv2lem5  5338  ralrnmptw  7027  ralrnmpt  7029  f1mpt  7195  mpo2eqb  7478  ralrnmpo  7485  naddcom  8597  naddrid  8598  naddass  8611  rankonidlem  9721  acni2  9937  kmlem8  10049  kmlem13  10054  fimaxre3  12068  cau3lem  15262  rlim2  15403  rlim0  15415  rlim0lt  15416  catpropd  17615  funcres2b  17804  ulmss  26333  lgamgulmlem6  26971  colinearalg  28888  axpasch  28919  axcontlem2  28943  axcontlem4  28945  axcontlem7  28948  axcontlem8  28949  neibastop3  36406  bj-0int  37145  ralbi12f  38210  iineq12f  38214  pmapglbx  39878  ordelordALTVD  44969