![]() |
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 2135, ax-11 2150, and ax-12 2163 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 2845 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | anbi12d 624 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) |
5 | 4 | rexbidv2 3233 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1601 ∈ wcel 2107 ∃wrex 3091 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-cleq 2770 df-clel 2774 df-rex 3096 |
This theorem is referenced by: rexeqbi1dv 3329 supeq123d 8644 fpwwe2lem13 9799 vdwpc 16088 ramval 16116 mreexexlemd 16690 iscat 16718 iscatd 16719 catidex 16720 gsumval2a 17665 ismnddef 17682 mndpropd 17702 isgrp 17815 isgrpd2e 17828 cayleyth 18218 psgnfval 18304 iscyg 18667 ltbval 19868 opsrval 19871 scmatval 20715 pmatcollpw3fi1lem2 20999 pmatcollpw3fi1 21000 neiptopnei 21344 is1stc 21653 2ndc1stc 21663 2ndcsep 21671 islly 21680 isnlly 21681 ucnval 22489 imasdsf1olem 22586 met2ndc 22736 evthicc 23663 istrkgld 25810 legval 25935 ishpg 26107 iscgra 26157 isinag 26187 isleag 26196 nbgrval 26683 nb3grprlem2 26729 1loopgrvd0 26852 erclwwlkeq 27407 eucrctshift 27647 isplig 27903 nmoofval 28189 reprsuc 31295 istrkg2d 31346 iscvm 31840 cvmlift2lem13 31896 br8 32240 br6 32241 br4 32242 brsegle 32804 hilbert1.1 32850 poimirlem26 34061 poimirlem28 34063 poimirlem29 34064 cover2g 34134 isexid 34270 isrngo 34320 isrngod 34321 isgrpda 34378 lshpset 35132 cvrfval 35422 isatl 35453 ishlat1 35506 llnset 35659 lplnset 35683 lvolset 35726 lineset 35892 lcfl7N 37655 lcfrlem8 37703 lcfrlem9 37704 lcf1o 37705 hvmapffval 37912 hvmapfval 37913 hvmapval 37914 prjspval 38204 mzpcompact2lem 38274 eldioph 38281 aomclem8 38590 clsk1independent 39300 ovnval 41682 sprval 42418 nnsum3primes4 42701 nnsum3primesprm 42703 nnsum3primesgbe 42705 wtgoldbnnsum4prm 42715 bgoldbnnsum3prm 42717 zlidlring 42943 uzlidlring 42944 lcoop 43215 ldepsnlinc 43312 nnpw2p 43395 lines 43467 |
Copyright terms: Public domain | W3C validator |