Theorem ralbi 3117

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  uniiunlem  4012  iineq2  4971  reusv2lem5  5363  ralrnmptw  7094  ralrnmpt  7096  f1mpt  7265  mpo2eqb  7552  ralrnmpo  7559  naddcom  8692  naddrid  8693  naddass  8706  rankonidlem  9838  acni2  10125  kmlem8  10236  kmlem13  10241  fimaxre3  12263  cau3lem  15522  rlim2  15663  rlim0  15675  rlim0lt  15676  catpropd  17883  funcres2b  18072  ulmss  26724  lgamgulmlem6  27361  colinearalg  29488  axpasch  29519  axcontlem2  29543  axcontlem4  29545  axcontlem7  29548  axcontlem8  29549  nmulrid  36946  neibastop3  37150  bj-0int  38022  ralbi12f  39093  iineq12f  39097  pmapglbx  40827  ordelordALTVD  45849