Theorem ralbi 3091

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

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

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

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

This theorem is referenced by:  uniiunlem  4060  iineq2  4986  reusv2lem5  5370  ralrnmptw  7081  ralrnmpt  7083  f1mpt  7250  mpo2eqb  7534  ralrnmpo  7541  naddcom  8689  naddrid  8690  naddass  8703  rankonidlem  9835  acni2  10053  kmlem8  10165  kmlem13  10170  fimaxre3  12181  cau3lem  15362  rlim2  15501  rlim0  15513  rlim0lt  15514  catpropd  17708  funcres2b  17897  ulmss  26345  lgamgulmlem6  26982  colinearalg  28823  axpasch  28854  axcontlem2  28878  axcontlem4  28880  axcontlem7  28883  axcontlem8  28884  neibastop3  36309  bj-0int  37048  ralbi12f  38113  iineq12f  38117  pmapglbx  39717  ordelordALTVD  44825