| 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 2141, ax-11 2157, and ax-12 2177 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 2827 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
| 3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 4 | 2, 3 | anbi12d 632 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) |
| 5 | 4 | rexbidv2 3175 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 ∃wrex 3070 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 df-rex 3071 |
| This theorem is referenced by: frd 5641 supeq123d 9490 fpwwe2lem12 10682 vdwpc 17018 ramval 17046 mreexexlemd 17687 iscat 17715 iscatd 17716 catidex 17717 gsumval2a 18698 ismnddef 18749 mndpropd 18772 isgrp 18957 isgrpd2e 18973 cayleyth 19433 psgnfval 19518 iscyg 19897 ltbval 22061 opsrval 22064 scmatval 22510 pmatcollpw3fi1lem2 22793 pmatcollpw3fi1 22794 neiptopnei 23140 is1stc 23449 2ndc1stc 23459 2ndcsep 23467 islly 23476 isnlly 23477 ucnval 24286 imasdsf1olem 24383 met2ndc 24536 evthicc 25494 elmade2 27907 addsval 27995 mulsval 28135 istrkgb 28463 istrkge 28465 istrkgld 28467 legval 28592 ishpg 28767 iscgra 28817 isinag 28846 isleag 28855 nbgrval 29353 nb3grprlem2 29398 1loopgrvd0 29522 erclwwlkeq 30037 eucrctshift 30262 isplig 30495 nmoofval 30781 erlval 33262 idomsubr 33311 elrsp 33400 1arithidom 33565 dfufd2lem 33577 fldextrspunlsp 33724 constrsuc 33779 reprsuc 34630 istrkg2d 34681 iscvm 35264 cvmlift2lem13 35320 br8 35756 br6 35757 br4 35758 brsegle 36109 hilbert1.1 36155 pibp21 37416 poimirlem26 37653 poimirlem28 37655 poimirlem29 37656 cover2g 37723 isexid 37854 isrngo 37904 isrngod 37905 isgrpda 37962 lshpset 38979 cvrfval 39269 isatl 39300 ishlat1 39353 llnset 39507 lplnset 39531 lvolset 39574 lineset 39740 lcfl7N 41503 lcfrlem8 41551 lcfrlem9 41552 lcf1o 41553 hvmapffval 41760 hvmapfval 41761 hvmapval 41762 prjspval 42613 mzpcompact2lem 42762 eldioph 42769 aomclem8 43073 tfsconcatun 43350 clsk1independent 44059 ovnval 46556 sprval 47466 nnsum3primes4 47775 nnsum3primesprm 47777 nnsum3primesgbe 47779 wtgoldbnnsum4prm 47789 bgoldbnnsum3prm 47791 clnbgrval 47809 gpg3kgrtriex 48045 zlidlring 48150 uzlidlring 48151 lcoop 48328 ldepsnlinc 48425 nnpw2p 48507 lines 48652 iscnrm3r 48845 |
| Copyright terms: Public domain | W3C validator |