Theorem ralbi 3085

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

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

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 3045

This theorem is referenced by:  uniiunlem  4050  iineq2  4976  reusv2lem5  5357  ralrnmptw  7066  ralrnmpt  7068  f1mpt  7236  mpo2eqb  7521  ralrnmpo  7528  naddcom  8646  naddrid  8647  naddass  8660  rankonidlem  9781  acni2  9999  kmlem8  10111  kmlem13  10116  fimaxre3  12129  cau3lem  15321  rlim2  15462  rlim0  15474  rlim0lt  15475  catpropd  17670  funcres2b  17859  ulmss  26306  lgamgulmlem6  26944  colinearalg  28837  axpasch  28868  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  neibastop3  36350  bj-0int  37089  ralbi12f  38154  iineq12f  38158  pmapglbx  39763  ordelordALTVD  44856