![]() |
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 rule). (Contributed by NM, 13-Nov-2004.) |
Ref | Expression |
---|---|
reubidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
reubidva | ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1883 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | reubidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | reubida 3154 | 1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∈ wcel 2030 ∃!wreu 2943 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-12 2087 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-nf 1750 df-eu 2502 df-reu 2948 |
This theorem is referenced by: reubidv 3156 reuxfr2d 4921 reuxfrd 4923 exfo 6417 f1ofveu 6685 zmax 11823 zbtwnre 11824 rebtwnz 11825 icoshftf1o 12333 divalgb 15174 1arith2 15679 ply1divalg2 23943 frgr2wwlkeu 27307 numclwwlk2lem1 27356 numclwlk2lem2f1o 27359 numclwwlk2lem1OLD 27363 numclwlk2lem2f1oOLD 27366 pjhtheu2 28403 reuxfr3d 29456 reuxfr4d 29457 xrsclat 29808 xrmulc1cn 30104 poimirlem25 33564 hdmap14lem14 37490 |
Copyright terms: Public domain | W3C validator |