Theorem ralbi 3091

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 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 1796  ax-4 1810

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

This theorem is referenced by:  uniiunlem  4039  iineq2  4967  reusv2lem5  5347  ralrnmptw  7039  ralrnmpt  7041  f1mpt  7207  mpo2eqb  7490  ralrnmpo  7497  naddcom  8610  naddrid  8611  naddass  8624  rankonidlem  9740  acni2  9956  kmlem8  10068  kmlem13  10073  fimaxre3  12088  cau3lem  15278  rlim2  15419  rlim0  15431  rlim0lt  15432  catpropd  17632  funcres2b  17821  ulmss  26362  lgamgulmlem6  27000  colinearalg  28983  axpasch  29014  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  neibastop3  36556  bj-0int  37306  ralbi12f  38361  iineq12f  38365  pmapglbx  40039  ordelordALTVD  45117