Theorem cbvriotavw 7118

Description: Change bound variable in a restricted description binder. Version of cbvriotav 7122 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 26-Jan-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		nfv 1915	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1915	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvriotavw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvriotaw 7117	1 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ℩crio 7107

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-sn 4523  df-uni 4799  df-iota 6294  df-riota 7108

This theorem is referenced by:  ordtypecbv  9014  fin23lem27  9788  zorn2g  9963  uspgredg2v  27113  usgredg2v  27116  cnlnadji  29958  nmopadjlei  29970  cvmliftlem15  32776  cvmliftiota  32779  cvmlift2  32794  cvmlift3lem7  32803  cvmlift3  32806  nosupcbv  33490  noinfcbv  33505  lshpkrlem3  36710  cdleme40v  38067  lcfl7N  39099  lcf1o  39149  lcfrlem39  39179  hdmap1cbv  39400  wessf1ornlem  42203  fourierdlem103  43239  fourierdlem104  43240