Theorem cbvriotavw 7354

Description: Change bound variable in a restricted description binder. Version of cbvriotav 7358 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by GG, 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 2811	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvriotavw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbviotavw 6472	. 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-riota 7344	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-riota 7344	. 2 ⊢ (℩𝑦 ∈ 𝐴 𝜓) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3eqtr4i 2762	1 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ℩cio 6462  ℩crio 7343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872  df-iota 6464  df-riota 7344

This theorem is referenced by:  ordtypecbv  9470  fin23lem27  10281  zorn2g  10456  nosupcbv  27614  noinfcbv  27629  uspgredg2v  29151  usgredg2v  29154  cnlnadji  32005  nmopadjlei  32017  cvmliftlem15  35285  cvmliftiota  35288  cvmlift2  35303  cvmlift3lem7  35312  cvmlift3  35315  weiunlem2  36451  lshpkrlem3  39105  cdleme40v  40463  lcfl7N  41495  lcf1o  41545  lcfrlem39  41575  hdmap1cbv  41796  wessf1ornlem  45179  fourierdlem103  46207  fourierdlem104  46208