Theorem ralbi 3083

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wral 3054

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

This theorem depends on definitions:  df-bi 210  df-ral 3059

This theorem is referenced by:  rexbi  3156  uniiunlem  3985  iineq2  4911  reusv2lem5  5279  ralrnmptw  6882  ralrnmpt  6884  f1mpt  7042  mpo2eqb  7310  ralrnmpo  7316  rankonidlem  9342  acni2  9558  kmlem8  9669  kmlem13  9674  fimaxre3  11676  cau3lem  14816  rlim2  14955  rlim0  14967  rlim0lt  14968  catpropd  17095  funcres2b  17284  ulmss  25156  lgamgulmlem6  25783  colinearalg  26868  axpasch  26899  axcontlem2  26923  axcontlem4  26925  axcontlem7  26928  axcontlem8  26929  naddcom  33490  naddid1  33491  neibastop3  34206  bj-0int  34925  ralbi12f  35973  iineq12f  35977  pmapglbx  37438  ordelordALTVD  42065