Theorem ralbi 3094

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wral 3053

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 208  df-ral 3054

This theorem is referenced by:  uniiunlem  4018  iineq2  4942  reusv2lem5  5331  ralrnmptw  7035  ralrnmpt  7037  f1mpt  7205  mpo2eqb  7488  ralrnmpo  7495  naddcom  8608  naddrid  8609  naddass  8622  rankonidlem  9743  acni2  9959  kmlem8  10071  kmlem13  10076  fimaxre3  12093  cau3lem  15308  rlim2  15449  rlim0  15461  rlim0lt  15462  catpropd  17666  funcres2b  17855  ulmss  26380  lgamgulmlem6  27015  colinearalg  28997  axpasch  29028  axcontlem2  29052  axcontlem4  29054  axcontlem7  29057  axcontlem8  29058  neibastop3  36590  bj-0int  37459  ralbi12f  38527  iineq12f  38531  pmapglbx  40261  ordelordALTVD  45310