![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexeqbidv | Structured version Visualization version GIF version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2129, ax-11 2146, and ax-12 2166 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
Ref | Expression |
---|---|
raleqbidv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
raleqbidv.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
rexeqbidv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleqbidv.1 | . . . 4 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | eleq2d 2815 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | anbi12d 630 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) |
5 | 4 | rexbidv2 3172 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ∈ wcel 2098 ∃wrex 3067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2720 df-clel 2806 df-rex 3068 |
This theorem is referenced by: frd 5641 supeq123d 9481 fpwwe2lem12 10673 vdwpc 16956 ramval 16984 mreexexlemd 17631 iscat 17659 iscatd 17660 catidex 17661 gsumval2a 18652 ismnddef 18703 mndpropd 18726 isgrp 18903 isgrpd2e 18919 cayleyth 19377 psgnfval 19462 iscyg 19841 ltbval 21988 opsrval 21991 scmatval 22426 pmatcollpw3fi1lem2 22709 pmatcollpw3fi1 22710 neiptopnei 23056 is1stc 23365 2ndc1stc 23375 2ndcsep 23383 islly 23392 isnlly 23393 ucnval 24202 imasdsf1olem 24299 met2ndc 24452 evthicc 25408 elmade2 27815 addsval 27899 mulsval 28029 istrkgb 28279 istrkge 28281 istrkgld 28283 legval 28408 ishpg 28583 iscgra 28633 isinag 28662 isleag 28671 nbgrval 29169 nb3grprlem2 29214 1loopgrvd0 29338 erclwwlkeq 29848 eucrctshift 30073 isplig 30306 nmoofval 30592 erlval 32997 idomsubr 33020 elrsp 33109 reprsuc 34280 istrkg2d 34331 iscvm 34902 cvmlift2lem13 34958 br8 35383 br6 35384 br4 35385 brsegle 35737 hilbert1.1 35783 pibp21 36927 poimirlem26 37152 poimirlem28 37154 poimirlem29 37155 cover2g 37222 isexid 37353 isrngo 37403 isrngod 37404 isgrpda 37461 lshpset 38482 cvrfval 38772 isatl 38803 ishlat1 38856 llnset 39010 lplnset 39034 lvolset 39077 lineset 39243 lcfl7N 41006 lcfrlem8 41054 lcfrlem9 41055 lcf1o 41056 hvmapffval 41263 hvmapfval 41264 hvmapval 41265 prjspval 42058 mzpcompact2lem 42202 eldioph 42209 aomclem8 42516 tfsconcatun 42797 clsk1independent 43507 ovnval 45958 sprval 46848 nnsum3primes4 47157 nnsum3primesprm 47159 nnsum3primesgbe 47161 wtgoldbnnsum4prm 47171 bgoldbnnsum3prm 47173 clnbgrval 47191 zlidlring 47374 uzlidlring 47375 lcoop 47557 ldepsnlinc 47654 nnpw2p 47737 lines 47882 iscnrm3r 48045 |
Copyright terms: Public domain | W3C validator |