Theorem ralbi 3096

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wral 3055

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

This theorem depends on definitions:  df-bi 209  df-ral 3056

This theorem is referenced by:  uniiunlem  4020  iineq2  4944  reusv2lem5  5333  ralrnmptw  7038  ralrnmpt  7040  f1mpt  7208  mpo2eqb  7491  ralrnmpo  7498  naddcom  8612  naddrid  8613  naddass  8626  rankonidlem  9747  acni2  9963  kmlem8  10075  kmlem13  10080  fimaxre3  12097  cau3lem  15312  rlim2  15453  rlim0  15465  rlim0lt  15466  catpropd  17670  funcres2b  17859  ulmss  26383  lgamgulmlem6  27018  colinearalg  28999  axpasch  29030  axcontlem2  29054  axcontlem4  29056  axcontlem7  29059  axcontlem8  29060  neibastop3  36603  bj-0int  37472  ralbi12f  38540  iineq12f  38544  pmapglbx  40274  ordelordALTVD  45323