Theorem cbvriotavw 7327

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ℩cio 6447  ℩crio 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-uni 4865  df-iota 6449  df-riota 7317

This theorem is referenced by:  ordtypecbv  9426  fin23lem27  10242  zorn2g  10417  nosupcbv  27674  noinfcbv  27689  uspgredg2v  29301  usgredg2v  29304  cnlnadji  32155  nmopadjlei  32167  cvmliftlem15  35494  cvmliftiota  35497  cvmlift2  35512  cvmlift3lem7  35521  cvmlift3  35524  weiunlem  36659  lshpkrlem3  39440  cdleme40v  40797  lcfl7N  41829  lcf1o  41879  lcfrlem39  41909  hdmap1cbv  42130  wessf1ornlem  45496  fourierdlem103  46520  fourierdlem104  46521