Theorem ralbi 3092

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

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

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

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

This theorem is referenced by:  uniiunlem  4062  iineq2  4988  reusv2lem5  5372  ralrnmptw  7084  ralrnmpt  7086  f1mpt  7254  mpo2eqb  7539  ralrnmpo  7546  naddcom  8694  naddrid  8695  naddass  8708  rankonidlem  9842  acni2  10060  kmlem8  10172  kmlem13  10177  fimaxre3  12188  cau3lem  15373  rlim2  15512  rlim0  15524  rlim0lt  15525  catpropd  17721  funcres2b  17910  ulmss  26358  lgamgulmlem6  26996  colinearalg  28889  axpasch  28920  axcontlem2  28944  axcontlem4  28946  axcontlem7  28949  axcontlem8  28950  neibastop3  36380  bj-0int  37119  ralbi12f  38184  iineq12f  38188  pmapglbx  39788  ordelordALTVD  44891