Theorem ralbi 3093

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 3077	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
3		biimpr 220	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
4	3	ral2imi 3077	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜑))
5	2, 4	impbid 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))

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

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 3053

This theorem is referenced by:  uniiunlem  4041  iineq2  4969  reusv2lem5  5349  ralrnmptw  7048  ralrnmpt  7050  f1mpt  7217  mpo2eqb  7500  ralrnmpo  7507  naddcom  8620  naddrid  8621  naddass  8634  rankonidlem  9752  acni2  9968  kmlem8  10080  kmlem13  10085  fimaxre3  12100  cau3lem  15290  rlim2  15431  rlim0  15443  rlim0lt  15444  catpropd  17644  funcres2b  17833  ulmss  26374  lgamgulmlem6  27012  colinearalg  28995  axpasch  29026  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  neibastop3  36578  bj-0int  37354  ralbi12f  38411  iineq12f  38415  pmapglbx  40145  ordelordALTVD  45222