Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reubidva | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 13-Nov-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 14-Jan-2023.) |
Ref | Expression |
---|---|
reubidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
reubidva | ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reubidva.1 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
2 | 1 | pm5.32da 582 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
3 | 2 | eubidv 2588 | . 2 ⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))) |
4 | df-reu 3061 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
5 | df-reu 3061 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜒 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)) | |
6 | 3, 4, 5 | 3bitr4g 317 | 1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2114 ∃!weu 2570 ∃!wreu 3056 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-mo 2541 df-eu 2571 df-reu 3061 |
This theorem is referenced by: reubidv 3293 reuxfrd 3652 reuxfr1d 3654 exfo 6894 f1ofveu 7178 zmax 12440 zbtwnre 12441 rebtwnz 12442 icoshftf1o 12961 divalgb 15862 1arith2 16377 ply1divalg2 24904 addsq2reu 26189 addsqn2reu 26190 addsqrexnreu 26191 2sqreultlem 26196 2sqreunnltlem 26199 frgr2wwlkeu 28277 numclwwlk2lem1 28326 numclwlk2lem2f1o 28329 pjhtheu2 29364 reuxfrdf 30426 xrsclat 30879 xrmulc1cn 31465 poimirlem25 35458 hdmap14lem14 39551 prproropreud 44543 quad1 44654 requad1 44656 requad2 44657 itscnhlinecirc02p 45713 |
Copyright terms: Public domain | W3C validator |