Theorem ralbi 3089

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

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

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

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

This theorem is referenced by:  uniiunlem  4037  iineq2  4965  reusv2lem5  5345  ralrnmptw  7037  ralrnmpt  7039  f1mpt  7205  mpo2eqb  7488  ralrnmpo  7495  naddcom  8608  naddrid  8609  naddass  8622  rankonidlem  9738  acni2  9954  kmlem8  10066  kmlem13  10071  fimaxre3  12086  cau3lem  15276  rlim2  15417  rlim0  15429  rlim0lt  15430  catpropd  17630  funcres2b  17819  ulmss  26360  lgamgulmlem6  26998  colinearalg  28932  axpasch  28963  axcontlem2  28987  axcontlem4  28989  axcontlem7  28992  axcontlem8  28993  neibastop3  36505  bj-0int  37245  ralbi12f  38300  iineq12f  38304  pmapglbx  39968  ordelordALTVD  45049