Theorem ralbi 3126

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

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

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

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

This theorem is referenced by:  uniiunlem  4049  iineq2  4981  reusv2lem5  5374  ralrnmptw  7090  ralrnmpt  7092  f1mpt  7260  mpo2eqb  7543  ralrnmpo  7550  naddcom  8669  naddrid  8670  naddass  8683  rankonidlem  9800  acni2  10030  kmlem8  10141  kmlem13  10146  fimaxre3  12161  cau3lem  15406  rlim2  15547  rlim0  15559  rlim0lt  15560  catpropd  17765  funcres2b  17954  ulmss  26526  lgamgulmlem6  27164  colinearalg  29201  axpasch  29232  axcontlem2  29256  axcontlem4  29258  axcontlem7  29261  axcontlem8  29262  neibastop3  36796  bj-0int  37665  ralbi12f  38733  iineq12f  38737  pmapglbx  40467  ordelordALTVD  45501