Theorem cbvriotavw 7375

Description: Change bound variable in a restricted description binder. Version of cbvriotav 7379 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 2843	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvriotavw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbviotavw 6491	. 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-riota 7365	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-riota 7365	. 2 ⊢ (℩𝑦 ∈ 𝐴 𝜓) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3eqtr4i 2793	1 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ℩cio 6481  ℩crio 7364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3915  df-uni 4867  df-iota 6483  df-riota 7365

This theorem is used by:  ordtypecbv  9489  fin23lem27  10377  zorn2g  10552  nosupcbv  27992  noinfcbv  28007  uspgredg2v  29738  usgredg2v  29741  cnlnadji  32611  nmopadjlei  32623  cvmliftlem15  35984  cvmliftiota  35987  cvmlift2  36002  cvmlift3lem7  36011  cvmlift3  36014  weiunlem  37173  lshpkrlem3  40089  cdleme40v  41446  lcfl7N  42478  lcf1o  42528  lcfrlem39  42558  hdmap1cbv  42779  wessf1ornlem  46121  fourierdlem103  47141  fourierdlem104  47142