Theorem ralbi 3109

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

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

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

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

This theorem is referenced by:  rexbiOLD  3111  uniiunlem  4110  iineq2  5035  reusv2lem5  5420  ralrnmptw  7128  ralrnmpt  7130  f1mpt  7298  mpo2eqb  7582  ralrnmpo  7589  naddcom  8738  naddrid  8739  naddass  8752  rankonidlem  9897  acni2  10115  kmlem8  10227  kmlem13  10232  fimaxre3  12241  cau3lem  15403  rlim2  15542  rlim0  15554  rlim0lt  15555  catpropd  17767  funcres2b  17961  ulmss  26458  lgamgulmlem6  27095  colinearalg  28943  axpasch  28974  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  neibastop3  36328  bj-0int  37067  ralbi12f  38120  iineq12f  38124  pmapglbx  39726  ordelordALTVD  44838