Theorem cbvriotavw 7375

Description: Change bound variable in a restricted description binder. Version of cbvriotav 7380 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 30-Sep-2024.)

Hypothesis

Ref	Expression
cbvriotavw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvriotavw	⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvriotavw

Step	Hyp	Ref	Expression
1		eleq1w 2817	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvriotavw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbviotavw 6504	. 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-riota 7365	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-riota 7365	. 2 ⊢ (℩𝑦 ∈ 𝐴 𝜓) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3eqtr4i 2771	1 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ℩cio 6494  ℩crio 7364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-iota 6496  df-riota 7365

This theorem is referenced by:  ordtypecbv  9512  fin23lem27  10323  zorn2g  10498  nosupcbv  27205  noinfcbv  27220  uspgredg2v  28481  usgredg2v  28484  cnlnadji  31329  nmopadjlei  31341  cvmliftlem15  34289  cvmliftiota  34292  cvmlift2  34307  cvmlift3lem7  34316  cvmlift3  34319  lshpkrlem3  37982  cdleme40v  39340  lcfl7N  40372  lcf1o  40422  lcfrlem39  40452  hdmap1cbv  40673  wessf1ornlem  43882  fourierdlem103  44925  fourierdlem104  44926